Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  nnsucuniel Unicode version

Theorem nnsucuniel 6345
 Description: Given an element of the union of a natural number , is an element of itself. The reverse direction holds for all ordinals (sucunielr 4386). The forward direction for all ordinals implies excluded middle (ordsucunielexmid 4406). (Contributed by Jim Kingdon, 13-Mar-2022.)
Assertion
Ref Expression
nnsucuniel

Proof of Theorem nnsucuniel
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 noel 3333 . . . . . . 7
2 uni0 3729 . . . . . . . 8
32eleq2i 2181 . . . . . . 7
41, 3mtbir 643 . . . . . 6
5 unieq 3711 . . . . . . 7
65eleq2d 2184 . . . . . 6
74, 6mtbiri 647 . . . . 5
87pm2.21d 591 . . . 4
10 unieq 3711 . . . . . . . . . . . 12
1110eleq2d 2184 . . . . . . . . . . 11
1211ad2antll 480 . . . . . . . . . 10
1312biimpa 292 . . . . . . . . 9
14 simplrl 507 . . . . . . . . . . 11
15 nnord 4485 . . . . . . . . . . . . 13
16 ordtr 4260 . . . . . . . . . . . . 13
1715, 16syl 14 . . . . . . . . . . . 12
18 vex 2660 . . . . . . . . . . . . 13
1918unisuc 4295 . . . . . . . . . . . 12
2017, 19sylib 121 . . . . . . . . . . 11
2114, 20syl 14 . . . . . . . . . 10
2221eleq2d 2184 . . . . . . . . 9
2313, 22mpbid 146 . . . . . . . 8
24 nnsucelsuc 6341 . . . . . . . . 9
2514, 24syl 14 . . . . . . . 8
2623, 25mpbid 146 . . . . . . 7
27 simplrr 508 . . . . . . 7
2826, 27eleqtrrd 2194 . . . . . 6
2928ex 114 . . . . 5
3029rexlimdvaa 2524 . . . 4
3130imp 123 . . 3
32 nn0suc 4478 . . 3
339, 31, 32mpjaodan 770 . 2
34 sucunielr 4386 . 2
3533, 34impbid1 141 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   wceq 1314   wcel 1463  wrex 2391  c0 3329  cuni 3702   wtr 3986   word 4244   csuc 4247  com 4464 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4006  ax-nul 4014  ax-pow 4058  ax-pr 4091  ax-un 4315  ax-iinf 4462 This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ral 2395  df-rex 2396  df-v 2659  df-dif 3039  df-un 3041  df-in 3043  df-ss 3050  df-nul 3330  df-pw 3478  df-sn 3499  df-pr 3500  df-uni 3703  df-int 3738  df-tr 3987  df-iord 4248  df-on 4250  df-suc 4253  df-iom 4465 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator