New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  nchoice GIF 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
Dummy variables m n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nchoicelem1 5481 . . . 4 (n Nn → ¬ n = ( Tc n +c 1c))
2 nchoicelem2 5482 . . . 4 (n Nn → ¬ n = ( Tc n +c 2c))
3 ioran 467 . . . 4 (¬ (n = ( Tc n +c 1c) n = ( Tc n +c 2c)) ↔ (¬ n = ( Tc n +c 1c) ¬ n = ( Tc n +c 2c)))
41, 2, 3sylanbrc 634 . . 3 (n Nn → ¬ (n = ( Tc n +c 1c) n = ( Tc n +c 2c)))
54nrex 2196 . 2 ¬ n Nn (n = ( Tc n +c 1c) n = ( Tc n +c 2c))
6 nchoicelem19 5499 . . 3 ( ≤c We NCm NC (( Spacm) Fin Tc m = m))
7 finnc 5455 . . . . . . . 8 (( Spacm) FinNc ( Spacm) Nn )
87biimpi 183 . . . . . . 7 (( Spacm) FinNc ( Spacm) Nn )
98ad2antrl 696 . . . . . 6 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → Nc ( Spacm) Nn )
10 simpll 702 . . . . . . . . 9 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → ≤c We NC )
11 simplr 703 . . . . . . . . 9 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → m NC )
12 simprl 704 . . . . . . . . 9 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → ( Spacm) Fin )
13 nchoicelem17 5497 . . . . . . . . 9 (( ≤c We NC m NC ( Spacm) Fin ) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))
1410, 11, 12, 13syl3anc 1125 . . . . . . . 8 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c))))
1514simprd 440 . . . . . . 7 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))
16 simprr 705 . . . . . . . . . . 11 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → Tc m = m)
1716fveq2d 4548 . . . . . . . . . 10 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → ( SpacTc m) = ( Spacm))
1817nceqd 5322 . . . . . . . . 9 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → Nc ( SpacTc m) = Nc ( Spacm))
1918eqeq1d 1903 . . . . . . . 8 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) ↔ Nc ( Spacm) = ( Tc Nc ( Spacm) +c 1c)))
2018eqeq1d 1903 . . . . . . . 8 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c) ↔ Nc ( Spacm) = ( Tc Nc ( Spacm) +c 2c)))
2119, 20orbi12d 677 . . . . . . 7 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → (( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)) ↔ ( Nc ( Spacm) = ( Tc Nc ( Spacm) +c 1c) Nc ( Spacm) = ( Tc Nc ( Spacm) +c 2c))))
2215, 21mpbid 198 . . . . . 6 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → ( Nc ( Spacm) = ( Tc Nc ( Spacm) +c 1c) Nc ( Spacm) = ( Tc Nc ( Spacm) +c 2c)))
23 id 18 . . . . . . . . 9 (n = Nc ( Spacm) → n = Nc ( Spacm))
24 tceq 5371 . . . . . . . . . 10 (n = Nc ( Spacm) → Tc n = Tc Nc ( Spacm))
2524addceq1d 3497 . . . . . . . . 9 (n = Nc ( Spacm) → ( Tc n +c 1c) = ( Tc Nc ( Spacm) +c 1c))
2623, 25eqeq12d 1909 . . . . . . . 8 (n = Nc ( Spacm) → (n = ( Tc n +c 1c) ↔ Nc ( Spacm) = ( Tc Nc ( Spacm) +c 1c)))
2724addceq1d 3497 . . . . . . . . 9 (n = Nc ( Spacm) → ( Tc n +c 2c) = ( Tc Nc ( Spacm) +c 2c))
2823, 27eqeq12d 1909 . . . . . . . 8 (n = Nc ( Spacm) → (n = ( Tc n +c 2c) ↔ Nc ( Spacm) = ( Tc Nc ( Spacm) +c 2c)))
2926, 28orbi12d 677 . . . . . . 7 (n = Nc ( Spacm) → ((n = ( Tc n +c 1c) n = ( Tc n +c 2c)) ↔ ( Nc ( Spacm) = ( Tc Nc ( Spacm) +c 1c) Nc ( Spacm) = ( Tc Nc ( Spacm) +c 2c))))
3029rcla4ev 2386 . . . . . 6 (( Nc ( Spacm) Nn ( Nc ( Spacm) = ( Tc Nc ( Spacm) +c 1c) Nc ( Spacm) = ( Tc Nc ( Spacm) +c 2c))) → n Nn (n = ( Tc n +c 1c) n = ( Tc n +c 2c)))
319, 22, 30syl2anc 631 . . . . 5 ((( ≤c We NC m NC ) (( Spacm) Fin Tc m = m)) → n Nn (n = ( Tc n +c 1c) n = ( Tc n +c 2c)))
3231ex 417 . . . 4 (( ≤c We NC m NC ) → ((( Spacm) Fin Tc m = m) → n Nn (n = ( Tc n +c 1c) n = ( Tc n +c 2c))))
3332rexlimdva 2218 . . 3 ( ≤c We NC → (m NC (( Spacm) Fin Tc m = m) → n Nn (n = ( Tc n +c 1c) n = ( Tc n +c 2c))))
346, 33mpd 13 . 2 ( ≤c We NCn Nn (n = ( Tc n +c 1c) n = ( Tc n +c 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   +c 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