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

Theorem vinf 3663
Description: The universe is infinite. Theorem X.1.63 of {{Rosser}}, p. 536.
Assertion
Ref Expression
vinf ¬ V Fin

Proof of Theorem vinf
StepHypRef Expression
1 noel 2731 . 2 ¬ Ncfin Spfin
2 spfinex 3645 . . . . . . . 8 Spfin V
3 ncfinprop 3582 . . . . . . . 8 ((V Fin Spfin V) → ( Ncfin Spfin Nn Spfin Ncfin Spfin ))
42, 3mpan2 641 . . . . . . 7 (V Fin → ( Ncfin Spfin Nn Spfin Ncfin Spfin ))
5 ne0i 2733 . . . . . . . 8 ( Spfin Ncfin SpfinNcfin Spfin)
65anim2i 542 . . . . . . 7 (( Ncfin Spfin Nn Spfin Ncfin Spfin ) → ( Ncfin Spfin Nn Ncfin Spfin))
74, 6syl 14 . . . . . 6 (V Fin → ( Ncfin Spfin Nn Ncfin Spfin))
8 eldifsn 2998 . . . . . 6 ( Ncfin Spfin ( Nn {}) ↔ ( Ncfin Spfin Nn Ncfin Spfin))
97, 8sylibr 200 . . . . 5 (V FinNcfin Spfin ( Nn {}))
10 evenoddnnnul 3622 . . . . 5 ( EvenfinOddfin ) = ( Nn {})
119, 10syl6eleqr 1979 . . . 4 (V FinNcfin Spfin ( EvenfinOddfin ))
12 vfinncsp 3662 . . . . . . . . . 10 (V FinNcfin Spfin = ( Tfin Ncfin Spfin +c 1c))
1312adantr 442 . . . . . . . . 9 ((V Fin Ncfin Spfin Evenfin ) → Ncfin Spfin = ( Tfin Ncfin Spfin +c 1c))
14 eventfin 3625 . . . . . . . . . . 11 ( Ncfin Spfin EvenfinTfin Ncfin Spfin Evenfin )
1514adantl 443 . . . . . . . . . 10 ((V Fin Ncfin Spfin Evenfin ) → Tfin Ncfin Spfin Evenfin )
16 evennnul 3616 . . . . . . . . . . . 12 ( Ncfin Spfin EvenfinNcfin Spfin)
1716adantl 443 . . . . . . . . . . 11 ((V Fin Ncfin Spfin Evenfin ) → Ncfin Spfin)
1813, 17eqnetrrd 2030 . . . . . . . . . 10 ((V Fin Ncfin Spfin Evenfin ) → ( Tfin Ncfin Spfin +c 1c) ≠ )
19 sucevenodd 3618 . . . . . . . . . 10 (( Tfin Ncfin Spfin Evenfin ( Tfin Ncfin Spfin +c 1c) ≠ ) → ( Tfin Ncfin Spfin +c 1c) Oddfin )
2015, 18, 19syl2anc 631 . . . . . . . . 9 ((V Fin Ncfin Spfin Evenfin ) → ( Tfin Ncfin Spfin +c 1c) Oddfin )
2113, 20eqeltrd 1968 . . . . . . . 8 ((V Fin Ncfin Spfin Evenfin ) → Ncfin Spfin Oddfin )
2221ex 417 . . . . . . 7 (V Fin → ( Ncfin Spfin EvenfinNcfin Spfin Oddfin ))
2322ancld 527 . . . . . 6 (V Fin → ( Ncfin Spfin Evenfin → ( Ncfin Spfin Evenfin Ncfin Spfin Oddfin )))
2412adantr 442 . . . . . . . . 9 ((V Fin Ncfin Spfin Oddfin ) → Ncfin Spfin = ( Tfin Ncfin Spfin +c 1c))
25 oddtfin 3626 . . . . . . . . . . 11 ( Ncfin Spfin OddfinTfin Ncfin Spfin Oddfin )
2625adantl 443 . . . . . . . . . 10 ((V Fin Ncfin Spfin Oddfin ) → Tfin Ncfin Spfin Oddfin )
27 oddnnul 3617 . . . . . . . . . . . 12 ( Ncfin Spfin OddfinNcfin Spfin)
2827adantl 443 . . . . . . . . . . 11 ((V Fin Ncfin Spfin Oddfin ) → Ncfin Spfin)
2924, 28eqnetrrd 2030 . . . . . . . . . 10 ((V Fin Ncfin Spfin Oddfin ) → ( Tfin Ncfin Spfin +c 1c) ≠ )
30 sucoddeven 3619 . . . . . . . . . 10 (( Tfin Ncfin Spfin Oddfin ( Tfin Ncfin Spfin +c 1c) ≠ ) → ( Tfin Ncfin Spfin +c 1c) Evenfin )
3126, 29, 30syl2anc 631 . . . . . . . . 9 ((V Fin Ncfin Spfin Oddfin ) → ( Tfin Ncfin Spfin +c 1c) Evenfin )
3224, 31eqeltrd 1968 . . . . . . . 8 ((V Fin Ncfin Spfin Oddfin ) → Ncfin Spfin Evenfin )
3332ex 417 . . . . . . 7 (V Fin → ( Ncfin Spfin OddfinNcfin Spfin Evenfin ))
3433ancrd 528 . . . . . 6 (V Fin → ( Ncfin Spfin Oddfin → ( Ncfin Spfin Evenfin Ncfin Spfin Oddfin )))
3523, 34jaod 366 . . . . 5 (V Fin → (( Ncfin Spfin Evenfin Ncfin Spfin Oddfin ) → ( Ncfin Spfin Evenfin Ncfin Spfin Oddfin )))
36 elun 2622 . . . . 5 ( Ncfin Spfin ( EvenfinOddfin ) ↔ ( Ncfin Spfin Evenfin Ncfin Spfin Oddfin ))
37 elin 2621 . . . . 5 ( Ncfin Spfin ( EvenfinOddfin ) ↔ ( Ncfin Spfin Evenfin Ncfin Spfin Oddfin ))
3835, 36, 373imtr4g 258 . . . 4 (V Fin → ( Ncfin Spfin ( EvenfinOddfin ) → Ncfin Spfin ( EvenfinOddfin )))
3911, 38mpd 13 . . 3 (V FinNcfin Spfin ( EvenfinOddfin ))
40 evenodddisj 3624 . . 3 ( EvenfinOddfin ) =
4139, 40syl6eleq 1978 . 2 (V FinNcfin Spfin )
421, 41mto 164 1 ¬ V Fin
Colors of variables: wff set class
Syntax hints:  ¬ wn 3   wo 354   wa 355   = wceq 1398   wcel 1400  wne 2012  Vcvv 2300   cdif 2608  cun 2609  cin 2610  c0 2726  {csn 2803  1cc1c 3238   Nn cnnc 3481   +c cplc 3483   Fin cfin 3484   Ncfin cncfin 3541   Tfin ctfin 3542   Evenfin cevenfin 3543   Oddfin coddfin 3544   Spfin cspfin 3546
This theorem is referenced by:  nulnnn  3664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  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-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-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-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-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
  Copyright terms: Public domain W3C validator