NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nnsucelr Unicode version

Theorem nnsucelr 4428
Description: Transfer membership in the successor of a natural into membership of the natural itself. Theorem X.1.17 of [Rosser] p. 525. (Contributed by SF, 14-Jan-2015.)
Hypotheses
Ref Expression
nnsucelr.1
nnsucelr.2
Assertion
Ref Expression
nnsucelr Nn 1c

Proof of Theorem nnsucelr
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnsucelrlem1 4424 . . . 4 1c
2 addceq1 4383 . . . . . . . . . 10 0c 1c 0c 1c
3 addcid2 4407 . . . . . . . . . 10 0c 1c 1c
42, 3syl6eq 2401 . . . . . . . . 9 0c 1c 1c
54eleq2d 2420 . . . . . . . 8 0c 1c 1c
6 el1c 4139 . . . . . . . 8 1c
75, 6syl6bb 252 . . . . . . 7 0c 1c
87anbi2d 684 . . . . . 6 0c 1c
9 eleq2 2414 . . . . . . 7 0c 0c
10 df-0c 4377 . . . . . . . . 9 0c
1110eleq2i 2417 . . . . . . . 8 0c
12 vex 2862 . . . . . . . . 9
1312elsnc 3756 . . . . . . . 8
1411, 13bitri 240 . . . . . . 7 0c
159, 14syl6bb 252 . . . . . 6 0c
168, 15imbi12d 311 . . . . 5 0c 1c
17162albidv 1627 . . . 4 0c 1c
18 addceq1 4383 . . . . . . . . 9 1c 1c
1918eleq2d 2420 . . . . . . . 8 1c 1c
2019anbi2d 684 . . . . . . 7 1c 1c
21 eleq2 2414 . . . . . . 7
2220, 21imbi12d 311 . . . . . 6 1c 1c
23222albidv 1627 . . . . 5 1c 1c
24 eleq12 2415 . . . . . . . . . 10
2524ancoms 439 . . . . . . . . 9
2625notbid 285 . . . . . . . 8
27 sneq 3744 . . . . . . . . . 10
28 uneq12 3413 . . . . . . . . . 10
2927, 28sylan2 460 . . . . . . . . 9
3029eleq1d 2419 . . . . . . . 8 1c 1c
3126, 30anbi12d 691 . . . . . . 7 1c 1c
32 eleq1 2413 . . . . . . . 8
3332adantr 451 . . . . . . 7
3431, 33imbi12d 311 . . . . . 6 1c 1c
3534cbval2v 2006 . . . . 5 1c 1c
3623, 35syl6bb 252 . . . 4 1c 1c
37 addceq1 4383 . . . . . . . 8 1c 1c 1c 1c
3837eleq2d 2420 . . . . . . 7 1c 1c 1c 1c
3938anbi2d 684 . . . . . 6 1c 1c 1c 1c
40 eleq2 2414 . . . . . 6 1c 1c
4139, 40imbi12d 311 . . . . 5 1c 1c 1c 1c 1c
42412albidv 1627 . . . 4 1c 1c 1c 1c 1c
43 addceq1 4383 . . . . . . . 8 1c 1c
4443eleq2d 2420 . . . . . . 7 1c 1c
4544anbi2d 684 . . . . . 6 1c 1c
46 eleq2 2414 . . . . . 6
4745, 46imbi12d 311 . . . . 5 1c 1c
48472albidv 1627 . . . 4 1c 1c
49 vex 2862 . . . . . . . . . . 11
5049unsneqsn 3887 . . . . . . . . . 10
5150ord 366 . . . . . . . . 9
5249snid 3760 . . . . . . . . . 10
53 eleq2 2414 . . . . . . . . . 10
5452, 53mpbiri 224 . . . . . . . . 9
5551, 54syl6 29 . . . . . . . 8
5655con1d 116 . . . . . . 7
5756exlimiv 1634 . . . . . 6
5857impcom 419 . . . . 5
5958gen2 1547 . . . 4
60 elsuc 4413 . . . . . . . . 9 1c 1c 1c
61 vex 2862 . . . . . . . . . . . . 13
6261elcompl 3225 . . . . . . . . . . . 12
6362anbi2i 675 . . . . . . . . . . 11 1c 1c
64 simprrl 740 . . . . . . . . . . . . . . . . . . 19 1c
65 sneq 3744 . . . . . . . . . . . . . . . . . . . 20
6665adantr 451 . . . . . . . . . . . . . . . . . . 19 1c
6764, 66difeq12d 3386 . . . . . . . . . . . . . . . . . 18 1c
68 simprrr 741 . . . . . . . . . . . . . . . . . . 19 1c
69 nnsucelrlem2 4425 . . . . . . . . . . . . . . . . . . 19
7068, 69syl 15 . . . . . . . . . . . . . . . . . 18 1c
71 simprlr 739 . . . . . . . . . . . . . . . . . . 19 1c
72 nnsucelrlem2 4425 . . . . . . . . . . . . . . . . . . 19
7371, 72syl 15 . . . . . . . . . . . . . . . . . 18 1c
7467, 70, 733eqtr3d 2393 . . . . . . . . . . . . . . . . 17 1c
75 simprll 738 . . . . . . . . . . . . . . . . 17 1c 1c
7674, 75eqeltrd 2427 . . . . . . . . . . . . . . . 16 1c 1c
77763adantr1 1114 . . . . . . . . . . . . . . 15 1c 1c 1c
7877ex 423 . . . . . . . . . . . . . 14 1c 1c 1c
79 simpl 443 . . . . . . . . . . . . . . . . 17 1c 1c
80 simpr3l 1016 . . . . . . . . . . . . . . . . 17 1c 1c
81 simpr2r 1015 . . . . . . . . . . . . . . . . 17 1c 1c
8249nnsucelrlem3 4426 . . . . . . . . . . . . . . . . 17
8379, 80, 81, 82syl3anc 1182 . . . . . . . . . . . . . . . 16 1c 1c
84 simp22r 1075 . . . . . . . . . . . . . . . . . . 19 1c 1c
85 difsn 3845 . . . . . . . . . . . . . . . . . . . . . . . 24
8685uneq1d 3417 . . . . . . . . . . . . . . . . . . . . . . 23
8786eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . 22
8887biimpcd 215 . . . . . . . . . . . . . . . . . . . . 21
89883ad2ant3 978 . . . . . . . . . . . . . . . . . . . 20 1c 1c
90 simp23l 1076 . . . . . . . . . . . . . . . . . . . . . 22 1c 1c
9190eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21 1c 1c
9261snss 3838 . . . . . . . . . . . . . . . . . . . . . . . 24
93 ssequn2 3436 . . . . . . . . . . . . . . . . . . . . . . . 24
9492, 93bitr2i 241 . . . . . . . . . . . . . . . . . . . . . . 23
9594biimpi 186 . . . . . . . . . . . . . . . . . . . . . 22
9695eqcoms 2356 . . . . . . . . . . . . . . . . . . . . 21
9791, 96syl6bi 219 . . . . . . . . . . . . . . . . . . . 20 1c 1c
9889, 97syld 40 . . . . . . . . . . . . . . . . . . 19 1c 1c
9984, 98mt3d 117 . . . . . . . . . . . . . . . . . 18 1c 1c
100 nnsucelrlem4 4427 . . . . . . . . . . . . . . . . . 18
10199, 100syl 15 . . . . . . . . . . . . . . . . 17 1c 1c
102 simpl3r 1011 . . . . . . . . . . . . . . . . . . . . 21 1c 1c
103 difss 3393 . . . . . . . . . . . . . . . . . . . . . 22
104103sseli 3269 . . . . . . . . . . . . . . . . . . . . 21
105102, 104nsyl 113 . . . . . . . . . . . . . . . . . . . 20 1c 1c
106 simp2l 981 . . . . . . . . . . . . . . . . . . . . 21 1c 1c 1c
107 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . 22 1c 1c
108107biimpd 198 . . . . . . . . . . . . . . . . . . . . 21 1c 1c
109106, 108mpan9 455 . . . . . . . . . . . . . . . . . . . 20 1c 1c 1c
110 simpl1 958 . . . . . . . . . . . . . . . . . . . . 21 1c 1c 1c
111 snex 4111 . . . . . . . . . . . . . . . . . . . . . . 23
11212, 111difex 4107 . . . . . . . . . . . . . . . . . . . . . 22
113 eleq12 2415 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
114113ancoms 439 . . . . . . . . . . . . . . . . . . . . . . . . . 26
115114notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . 25
116 sneq 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
117 uneq12 3413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
118116, 117sylan2 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26
119118eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . 25 1c 1c
120115, 119anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . 24 1c 1c
121 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . . . . 25
122121adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24
123120, 122imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . 23 1c 1c
124123spc2gv 2942 . . . . . . . . . . . . . . . . . . . . . 22 1c 1c
125112, 49, 124mp2an 653 . . . . . . . . . . . . . . . . . . . . 21 1c 1c
126110, 125syl 15 . . . . . . . . . . . . . . . . . . . 20 1c 1c 1c
127105, 109, 126mp2and 660 . . . . . . . . . . . . . . . . . . 19 1c 1c
1281273adant1 973 . . . . . . . . . . . . . . . . . 18 1c 1c
12961snid 3760 . . . . . . . . . . . . . . . . . . . . 21
130 eldif 3221 . . . . . . . . . . . . . . . . . . . . . 22
131130simprbi 450 . . . . . . . . . . . . . . . . . . . . 21
132129, 131mt2 170 . . . . . . . . . . . . . . . . . . . 20
13361elcompl 3225 . . . . . . . . . . . . . . . . . . . 20
134132, 133mpbir 200 . . . . . . . . . . . . . . . . . . 19
135 eqid 2353 . . . . . . . . . . . . . . . . . . 19
136 sneq 3744 . . . . . . . . . . . . . . . . . . . . . 22
137136uneq2d 3418 . . . . . . . . . . . . . . . . . . . . 21
138137eqeq2d 2364 . . . . . . . . . . . . . . . . . . . 20
139138rspcev 2955 . . . . . . . . . . . . . . . . . . 19
140134, 135, 139mp2an 653 . . . . . . . . . . . . . . . . . 18
141 compleq 3243 . . . . . . . . . . . . . . . . . . . . 21
142 uneq1 3411 . . . . . . . . . . . . . . . . . . . . . 22
143142eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21
144141, 143rexeqbidv 2820 . . . . . . . . . . . . . . . . . . . 20
145144rspcev 2955 . . . . . . . . . . . . . . . . . . 19
146 elsuc 4413 . . . . . . . . . . . . . . . . . . 19 1c
147145, 146sylibr 203 . . . . . . . . . . . . . . . . . 18 1c
148128, 140, 147sylancl 643 . . . . . . . . . . . . . . . . 17 1c 1c 1c
149101, 148eqeltrrd 2428 . . . . . . . . . . . . . . . 16 1c 1c 1c
15083, 149mpd3an3 1278 . . . . . . . . . . . . . . 15 1c 1c 1c
151150ex 423 . . . . . . . . . . . . . 14 1c 1c 1c
15278, 151pm2.61ine 2592 . . . . . . . . . . . . 13 1c 1c 1c
1531523expa 1151 . . . . . . . . . . . 12 1c 1c 1c
154153exp32 588 . . . . . . . . . . 11 1c 1c 1c
15563, 154sylan2b 461 . . . . . . . . . 10 1c 1c 1c
156155rexlimdvva 2745 . . . . . . . . 9 1c 1c 1c
15760, 156syl5bi 208 . . . . . . . 8 1c 1c 1c 1c
158157com23 72 . . . . . . 7 1c 1c 1c 1c
159158imp3a 420 . . . . . 6 1c 1c 1c 1c
160159alrimivv 1632 . . . . 5 1c 1c 1c 1c
161160a1i 10 . . . 4 Nn 1c 1c 1c 1c
1621, 17, 36, 42, 48, 59, 161finds 4411 . . 3 Nn 1c
163 nnsucelr.2 . . . . 5
164 eleq1 2413 . . . . . . . 8
165164notbid 285 . . . . . . 7
166 sneq 3744 . . . . . . . . 9
167166uneq2d 3418 . . . . . . . 8
168167eleq1d 2419 . . . . . . 7 1c 1c
169165, 168anbi12d 691 . . . . . 6 1c 1c
170169imbi1d 308 . . . . 5 1c 1c
171163, 170spcv 2945 . . . 4 1c 1c
172171alimi 1559 . . 3 1c 1c
173 nnsucelr.1 . . . 4
174 eleq2 2414 . . . . . . 7
175174notbid 285 . . . . . 6
176 uneq1 3411 . . . . . . 7
177176eleq1d 2419 . . . . . 6 1c 1c
178175, 177anbi12d 691 . . . . 5 1c 1c
179 eleq1 2413 . . . . 5
180178, 179imbi12d 311 . . . 4 1c 1c
181173, 180spcv 2945 . . 3 1c 1c
182162, 172, 1813syl 18 . 2 Nn 1c
183182imp 418 1 Nn 1c
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4   wb 176   wa 358   w3a 934  wal 1540  wex 1541   wceq 1642   wcel 1710   wne 2516  wrex 2615  cvv 2859   ∼ ccompl 3205   cdif 3206   cun 3207   wss 3257  c0 3550  csn 3737  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   cplc 4375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-0c 4377  df-addc 4378  df-nnc 4379
This theorem is referenced by:  nndisjeq  4429  prepeano4  4451  ssfin  4470
  Copyright terms: Public domain W3C validator