ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nnsucsssuc Structured version   GIF version

Theorem nnsucsssuc 5982
Description: Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4180, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4192. (Contributed by Jim Kingdon, 25-Aug-2019.)
Assertion
Ref Expression
nnsucsssuc ((A 𝜔 B 𝜔) → (AB ↔ suc A ⊆ suc B))

Proof of Theorem nnsucsssuc
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 2939 . . . . . 6 (x = A → (xBAB))
2 suceq 4084 . . . . . . 7 (x = A → suc x = suc A)
32sseq1d 2945 . . . . . 6 (x = A → (suc x ⊆ suc B ↔ suc A ⊆ suc B))
41, 3imbi12d 223 . . . . 5 (x = A → ((xB → suc x ⊆ suc B) ↔ (AB → suc A ⊆ suc B)))
54imbi2d 219 . . . 4 (x = A → ((B 𝜔 → (xB → suc x ⊆ suc B)) ↔ (B 𝜔 → (AB → suc A ⊆ suc B))))
6 sseq1 2939 . . . . . 6 (x = ∅ → (xB ↔ ∅ ⊆ B))
7 suceq 4084 . . . . . . 7 (x = ∅ → suc x = suc ∅)
87sseq1d 2945 . . . . . 6 (x = ∅ → (suc x ⊆ suc B ↔ suc ∅ ⊆ suc B))
96, 8imbi12d 223 . . . . 5 (x = ∅ → ((xB → suc x ⊆ suc B) ↔ (∅ ⊆ B → suc ∅ ⊆ suc B)))
10 sseq1 2939 . . . . . 6 (x = y → (xByB))
11 suceq 4084 . . . . . . 7 (x = y → suc x = suc y)
1211sseq1d 2945 . . . . . 6 (x = y → (suc x ⊆ suc B ↔ suc y ⊆ suc B))
1310, 12imbi12d 223 . . . . 5 (x = y → ((xB → suc x ⊆ suc B) ↔ (yB → suc y ⊆ suc B)))
14 sseq1 2939 . . . . . 6 (x = suc y → (xB ↔ suc yB))
15 suceq 4084 . . . . . . 7 (x = suc y → suc x = suc suc y)
1615sseq1d 2945 . . . . . 6 (x = suc y → (suc x ⊆ suc B ↔ suc suc y ⊆ suc B))
1714, 16imbi12d 223 . . . . 5 (x = suc y → ((xB → suc x ⊆ suc B) ↔ (suc yB → suc suc y ⊆ suc B)))
18 peano3 4242 . . . . . . . . 9 (B 𝜔 → suc B ≠ ∅)
1918neneqd 2201 . . . . . . . 8 (B 𝜔 → ¬ suc B = ∅)
20 peano2 4241 . . . . . . . . . 10 (B 𝜔 → suc B 𝜔)
21 0elnn 4263 . . . . . . . . . 10 (suc B 𝜔 → (suc B = ∅ suc B))
2220, 21syl 14 . . . . . . . . 9 (B 𝜔 → (suc B = ∅ suc B))
2322ord 630 . . . . . . . 8 (B 𝜔 → (¬ suc B = ∅ → ∅ suc B))
2419, 23mpd 13 . . . . . . 7 (B 𝜔 → ∅ suc B)
25 nnord 4257 . . . . . . . 8 (B 𝜔 → Ord B)
26 ordsucim 4172 . . . . . . . 8 (Ord B → Ord suc B)
27 0ex 3854 . . . . . . . . 9 V
28 ordelsuc 4177 . . . . . . . . 9 ((∅ V Ord suc B) → (∅ suc B ↔ suc ∅ ⊆ suc B))
2927, 28mpan 402 . . . . . . . 8 (Ord suc B → (∅ suc B ↔ suc ∅ ⊆ suc B))
3025, 26, 293syl 17 . . . . . . 7 (B 𝜔 → (∅ suc B ↔ suc ∅ ⊆ suc B))
3124, 30mpbid 135 . . . . . 6 (B 𝜔 → suc ∅ ⊆ suc B)
3231a1d 22 . . . . 5 (B 𝜔 → (∅ ⊆ B → suc ∅ ⊆ suc B))
33 simp3 892 . . . . . . . . . 10 (((y 𝜔 B 𝜔) (yB → suc y ⊆ suc B) suc yB) → suc yB)
34 simp1l 914 . . . . . . . . . . 11 (((y 𝜔 B 𝜔) (yB → suc y ⊆ suc B) suc yB) → y 𝜔)
35 simp1r 915 . . . . . . . . . . . 12 (((y 𝜔 B 𝜔) (yB → suc y ⊆ suc B) suc yB) → B 𝜔)
3635, 25syl 14 . . . . . . . . . . 11 (((y 𝜔 B 𝜔) (yB → suc y ⊆ suc B) suc yB) → Ord B)
37 ordelsuc 4177 . . . . . . . . . . 11 ((y 𝜔 Ord B) → (y B ↔ suc yB))
3834, 36, 37syl2anc 393 . . . . . . . . . 10 (((y 𝜔 B 𝜔) (yB → suc y ⊆ suc B) suc yB) → (y B ↔ suc yB))
3933, 38mpbird 156 . . . . . . . . 9 (((y 𝜔 B 𝜔) (yB → suc y ⊆ suc B) suc yB) → y B)
40 nnsucelsuc 5981 . . . . . . . . . 10 (B 𝜔 → (y B ↔ suc y suc B))
4135, 40syl 14 . . . . . . . . 9 (((y 𝜔 B 𝜔) (yB → suc y ⊆ suc B) suc yB) → (y B ↔ suc y suc B))
4239, 41mpbid 135 . . . . . . . 8 (((y 𝜔 B 𝜔) (yB → suc y ⊆ suc B) suc yB) → suc y suc B)
43 peano2 4241 . . . . . . . . . 10 (y 𝜔 → suc y 𝜔)
4434, 43syl 14 . . . . . . . . 9 (((y 𝜔 B 𝜔) (yB → suc y ⊆ suc B) suc yB) → suc y 𝜔)
4536, 26syl 14 . . . . . . . . 9 (((y 𝜔 B 𝜔) (yB → suc y ⊆ suc B) suc yB) → Ord suc B)
46 ordelsuc 4177 . . . . . . . . 9 ((suc y 𝜔 Ord suc B) → (suc y suc B ↔ suc suc y ⊆ suc B))
4744, 45, 46syl2anc 393 . . . . . . . 8 (((y 𝜔 B 𝜔) (yB → suc y ⊆ suc B) suc yB) → (suc y suc B ↔ suc suc y ⊆ suc B))
4842, 47mpbid 135 . . . . . . 7 (((y 𝜔 B 𝜔) (yB → suc y ⊆ suc B) suc yB) → suc suc y ⊆ suc B)
49483expia 1090 . . . . . 6 (((y 𝜔 B 𝜔) (yB → suc y ⊆ suc B)) → (suc yB → suc suc y ⊆ suc B))
5049exp31 346 . . . . 5 (y 𝜔 → (B 𝜔 → ((yB → suc y ⊆ suc B) → (suc yB → suc suc y ⊆ suc B))))
519, 13, 17, 32, 50finds2 4247 . . . 4 (x 𝜔 → (B 𝜔 → (xB → suc x ⊆ suc B)))
525, 51vtoclga 2592 . . 3 (A 𝜔 → (B 𝜔 → (AB → suc A ⊆ suc B)))
5352imp 115 . 2 ((A 𝜔 B 𝜔) → (AB → suc A ⊆ suc B))
54 nnon 4255 . . 3 (A 𝜔 → A On)
55 onsucsssucr 4180 . . 3 ((A On Ord B) → (suc A ⊆ suc BAB))
5654, 25, 55syl2an 273 . 2 ((A 𝜔 B 𝜔) → (suc A ⊆ suc BAB))
5753, 56impbid 120 1 ((A 𝜔 B 𝜔) → (AB ↔ suc A ⊆ suc B))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97  wb 98   wo 616   w3a 871   = wceq 1226   wcel 1370  Vcvv 2531  wss 2890  c0 3197  Ord word 4044  Oncon0 4045  suc csuc 4047  𝜔com 4236
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-nul 3853  ax-pow 3897  ax-pr 3914  ax-un 4116  ax-iinf 4234
This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ne 2184  df-ral 2285  df-rex 2286  df-v 2533  df-dif 2893  df-un 2895  df-in 2897  df-ss 2904  df-nul 3198  df-pw 3332  df-sn 3352  df-pr 3353  df-uni 3551  df-int 3586  df-tr 3825  df-iord 4048  df-on 4050  df-suc 4053  df-iom 4237
This theorem is referenced by:  nnaword  5991
  Copyright terms: Public domain W3C validator