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

Theorem nchoice 5500
Description: Cardinal less than or equal does not well-order the cardinals. This is equivalent to saying that the axiom of choice from ZFC is false in NF. Theorem 7.5 of {{Specker}}.
Assertion
Ref Expression
nchoice <_c We NC

Proof of Theorem nchoice
StepHypRef Expression
1 nchoicelem1 5481 . . . 4 Nn Tc 1c
2 nchoicelem2 5482 . . . 4 Nn Tc 2c
3 ioran 467 . . . 4 Tc 1c Tc 2c Tc 1c Tc 2c
41, 2, 3sylanbrc 634 . . 3 Nn Tc 1c Tc 2c
54nrex 2196 . 2 Nn Tc 1c Tc 2c
6 nchoicelem19 5499 . . 3 <_c We NC NC Spac Fin Tc
7 finnc 5455 . . . . . . . 8 Spac Fin Nc Spac Nn
87biimpi 183 . . . . . . 7 Spac Fin Nc Spac Nn
98ad2antrl 696 . . . . . 6 <_c We NC NC Spac Fin Tc Nc Spac Nn
10 simpll 702 . . . . . . . . 9 <_c We NC NC Spac Fin Tc <_c We NC
11 simplr 703 . . . . . . . . 9 <_c We NC NC Spac Fin Tc NC
12 simprl 704 . . . . . . . . 9 <_c We NC NC Spac Fin Tc Spac Fin
13 nchoicelem17 5497 . . . . . . . . 9 <_c We NC NC Spac Fin Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
1410, 11, 12, 13syl3anc 1125 . . . . . . . 8 <_c We NC NC Spac Fin Tc Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
1514simprd 440 . . . . . . 7 <_c We NC NC Spac Fin Tc Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
16 simprr 705 . . . . . . . . . . 11 <_c We NC NC Spac Fin Tc Tc
1716fveq2d 4548 . . . . . . . . . 10 <_c We NC NC Spac Fin Tc Spac Tc Spac
1817nceqd 5322 . . . . . . . . 9 <_c We NC NC Spac Fin Tc Nc Spac Tc Nc Spac
1918eqeq1d 1903 . . . . . . . 8 <_c We NC NC Spac Fin Tc Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Nc Spac 1c
2018eqeq1d 1903 . . . . . . . 8 <_c We NC NC Spac Fin Tc Nc Spac Tc Tc Nc Spac 2c Nc Spac Tc Nc Spac 2c
2119, 20orbi12d 677 . . . . . . 7 <_c We NC NC Spac Fin Tc Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nc Spac Tc Nc Spac 1c Nc Spac Tc Nc Spac 2c
2215, 21mpbid 198 . . . . . 6 <_c We NC NC Spac Fin Tc Nc Spac Tc Nc Spac 1c Nc Spac Tc Nc Spac 2c
23 id 18 . . . . . . . . 9 Nc Spac Nc Spac
24 tceq 5371 . . . . . . . . . 10 Nc Spac Tc Tc Nc Spac
2524addceq1d 3497 . . . . . . . . 9 Nc Spac Tc 1c Tc Nc Spac 1c
2623, 25eqeq12d 1909 . . . . . . . 8 Nc Spac Tc 1c Nc Spac Tc Nc Spac 1c
2724addceq1d 3497 . . . . . . . . 9 Nc Spac Tc 2c Tc Nc Spac 2c
2823, 27eqeq12d 1909 . . . . . . . 8 Nc Spac Tc 2c Nc Spac Tc Nc Spac 2c
2926, 28orbi12d 677 . . . . . . 7 Nc Spac Tc 1c Tc 2c Nc Spac Tc Nc Spac 1c Nc Spac Tc Nc Spac 2c
3029rcla4ev 2386 . . . . . 6 Nc Spac Nn Nc Spac Tc Nc Spac 1c Nc Spac Tc Nc Spac 2c Nn Tc 1c Tc 2c
319, 22, 30syl2anc 631 . . . . 5 <_c We NC NC Spac Fin Tc Nn Tc 1c Tc 2c
3231ex 417 . . . 4 <_c We NC NC Spac Fin Tc Nn Tc 1c Tc 2c
3332rexlimdva 2218 . . 3 <_c We NC NC Spac Fin Tc Nn Tc 1c Tc 2c
346, 33mpd 13 . 2 <_c We NC Nn Tc 1c Tc 2c
355, 34mto 164 1 <_c We NC
Colors of variables: wff set class
Syntax hints:   wn 3   wo 354   wa 355   wceq 1398   wcel 1400  wrex 2104  1cc1c 3238   Nn cnnc 3481   cplc 3483   Fin cfin 3484   class class class wbr 3736  cfv 3954   We cwe 5106   NC cncs 5300   <_c clec 5301   Nc cnc 5303   Tc ctc 5305  2cc2c 5306   Spac cspac 5465
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-meredith 1230  ax-5 1323  ax-6 1324  ax-7 1325  ax-gen 1326  ax-8 1402  ax-10 1403  ax-11 1404  ax-12 1405  ax-13 1406  ax-14 1407  ax-17 1413  ax-9 1424  ax-4 1429  ax-6o 1434  ax-16 1606  ax-ext 1877  ax-nin 3180  ax-xp 3181  ax-cnv 3182  ax-1c 3183  ax-sset 3184  ax-si 3185  ax-ins2 3186  ax-ins3 3187  ax-typlower 3188  ax-sn 3189
This theorem depends on definitions:  df-bi 174  df-or 356  df-an 357  df-3or 885  df-3an 886  df-nand 1259  df-tru 1301  df-ex 1328  df-sb 1568  df-eu 1795  df-mo 1796  df-clab 1883  df-cleq 1888  df-clel 1891  df-ne 2014  df-ral 2107  df-rex 2108  df-reu 2109  df-rab 2110  df-v 2302  df-sbc 2469  df-csb 2551  df-nin 2613  df-compl 2614  df-in 2615  df-un 2616  df-dif 2617  df-symdif 2618  df-nul 2727  df-sn 2807  df-pr 2808  df-tp 2809  df-opk 2863  df-ss 2876  df-pss 2878  df-uni 3038  df-int 3072  df-if 3109  df-pw 3167  df-1c 3240  df-pw1 3241  df-uni1 3242  df-xpk 3289  df-cnvk 3290  df-ins2k 3291  df-ins3k 3292  df-imak 3293  df-cok 3294  df-p6 3295  df-sik 3296  df-ssetk 3297  df-imagek 3298  df-idk 3299  df-iota 3450  df-0c 3485  df-addc 3486  df-nnc 3487  df-fin 3488  df-lefin 3547  df-ltfin 3548  df-ncfin 3549  df-tfin 3550  df-evenfin 3551  df-oddfin 3552  df-sfin 3553  df-spfin 3554  df-phi 3673  df-op 3674  df-proj1 3675  df-proj2 3676  df-opab 3723  df-br 3737  df-1st 3821  df-swap 3822  df-sset 3823  df-co 3824  df-ima 3825  df-si 3826  df-id 3939  df-xp 3957  df-rel 3958  df-cnv 3959  df-rn 3960  df-dm 3961  df-res 3962  df-fun 3963  df-fn 3964  df-f 3965  df-f1 3966  df-fo 3967  df-f1o 3968  df-fv 3969  df-2nd 3971  df-ov 4768  df-oprab 4769  df-mpt 4895  df-mpt2 4896  df-txp 4978  df-fix 4980  df-cup 4981  df-disj 4982  df-addcfn 4983  df-ins2 4984  df-ins3 4985  df-image 4986  df-ins4 4987  df-si3 4988  df-funs 4989  df-fns 4990  df-pw1fn 4992  df-fullfun 4993  df-clos1 5086  df-trans 5110  df-ref 5111  df-antisym 5112  df-partial 5113  df-connex 5114  df-strict 5115  df-found 5116  df-we 5117  df-sym 5119  df-er 5120  df-ec 5158  df-qs 5162  df-map 5213  df-en 5241  df-ncs 5310  df-lec 5311  df-ltc 5312  df-nc 5313  df-tc 5315  df-2c 5316  df-3c 5317  df-ce 5318  df-tcfn 5319  df-spac 5466
  Copyright terms: Public domain W3C validator