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

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

Proof of Theorem vinf
StepHypRef Expression
1 noel 2731 . 2 Ncfin Spfin
2 spfinex 3645 . . . . . . . 8 Spfin
3 ncfinprop 3582 . . . . . . . 8 Fin Spfin Ncfin Spfin Nn Spfin Ncfin Spfin
42, 3mpan2 641 . . . . . . 7 Fin Ncfin Spfin Nn Spfin Ncfin Spfin
5 ne0i 2733 . . . . . . . 8 Spfin Ncfin Spfin Ncfin Spfin
65anim2i 542 . . . . . . 7 Ncfin Spfin Nn Spfin Ncfin Spfin Ncfin Spfin Nn Ncfin Spfin
74, 6syl 14 . . . . . 6 Fin Ncfin Spfin Nn Ncfin Spfin
8 eldifsn 2998 . . . . . 6 Ncfin Spfin Nn Ncfin Spfin Nn Ncfin Spfin
97, 8sylibr 200 . . . . 5 Fin Ncfin Spfin Nn
10 evenoddnnnul 3622 . . . . 5 Evenfin Oddfin Nn
119, 10syl6eleqr 1979 . . . 4 Fin Ncfin Spfin Evenfin Oddfin
12 vfinncsp 3662 . . . . . . . . . 10 Fin Ncfin Spfin Tfin Ncfin Spfin 1c
1312adantr 442 . . . . . . . . 9 Fin Ncfin Spfin Evenfin Ncfin Spfin Tfin Ncfin Spfin 1c
14 eventfin 3625 . . . . . . . . . . 11 Ncfin Spfin Evenfin Tfin Ncfin Spfin Evenfin
1514adantl 443 . . . . . . . . . 10 Fin Ncfin Spfin Evenfin Tfin Ncfin Spfin Evenfin
16 evennnul 3616 . . . . . . . . . . . 12 Ncfin Spfin Evenfin Ncfin Spfin
1716adantl 443 . . . . . . . . . . 11 Fin Ncfin Spfin Evenfin Ncfin Spfin
1813, 17eqnetrrd 2030 . . . . . . . . . 10 Fin Ncfin Spfin Evenfin Tfin Ncfin Spfin 1c
19 sucevenodd 3618 . . . . . . . . . 10 Tfin Ncfin Spfin Evenfin Tfin Ncfin Spfin 1c Tfin Ncfin Spfin 1c Oddfin
2015, 18, 19syl2anc 631 . . . . . . . . 9 Fin Ncfin Spfin Evenfin Tfin Ncfin Spfin 1c Oddfin
2113, 20eqeltrd 1968 . . . . . . . 8 Fin Ncfin Spfin Evenfin Ncfin Spfin Oddfin
2221ex 417 . . . . . . 7 Fin Ncfin Spfin Evenfin Ncfin Spfin Oddfin
2322ancld 527 . . . . . 6 Fin Ncfin Spfin Evenfin Ncfin Spfin Evenfin Ncfin Spfin Oddfin
2412adantr 442 . . . . . . . . 9 Fin Ncfin Spfin Oddfin Ncfin Spfin Tfin Ncfin Spfin 1c
25 oddtfin 3626 . . . . . . . . . . 11 Ncfin Spfin Oddfin Tfin Ncfin Spfin Oddfin
2625adantl 443 . . . . . . . . . 10 Fin Ncfin Spfin Oddfin Tfin Ncfin Spfin Oddfin
27 oddnnul 3617 . . . . . . . . . . . 12 Ncfin Spfin Oddfin Ncfin Spfin
2827adantl 443 . . . . . . . . . . 11 Fin Ncfin Spfin Oddfin Ncfin Spfin
2924, 28eqnetrrd 2030 . . . . . . . . . 10 Fin Ncfin Spfin Oddfin Tfin Ncfin Spfin 1c
30 sucoddeven 3619 . . . . . . . . . 10 Tfin Ncfin Spfin Oddfin Tfin Ncfin Spfin 1c Tfin Ncfin Spfin 1c Evenfin
3126, 29, 30syl2anc 631 . . . . . . . . 9 Fin Ncfin Spfin Oddfin Tfin Ncfin Spfin 1c Evenfin
3224, 31eqeltrd 1968 . . . . . . . 8 Fin Ncfin Spfin Oddfin Ncfin Spfin Evenfin
3332ex 417 . . . . . . 7 Fin Ncfin Spfin Oddfin Ncfin Spfin Evenfin
3433ancrd 528 . . . . . 6 Fin Ncfin Spfin Oddfin Ncfin Spfin Evenfin Ncfin Spfin Oddfin
3523, 34jaod 366 . . . . 5 Fin Ncfin Spfin Evenfin Ncfin Spfin Oddfin Ncfin Spfin Evenfin Ncfin Spfin Oddfin
36 elun 2622 . . . . 5 Ncfin Spfin Evenfin Oddfin Ncfin Spfin Evenfin Ncfin Spfin Oddfin
37 elin 2621 . . . . 5 Ncfin Spfin Evenfin Oddfin Ncfin Spfin Evenfin Ncfin Spfin Oddfin
3835, 36, 373imtr4g 258 . . . 4 Fin Ncfin Spfin Evenfin Oddfin Ncfin Spfin Evenfin Oddfin
3911, 38mpd 13 . . 3 Fin Ncfin Spfin Evenfin Oddfin
40 evenodddisj 3624 . . 3 Evenfin Oddfin
4139, 40syl6eleq 1978 . 2 Fin Ncfin Spfin
421, 41mto 164 1 Fin
Colors of variables: wff set class
Syntax hints:   wn 3   wo 354   wa 355   wceq 1398   wcel 1400   wne 2012  cvv 2300   cdif 2608   cun 2609   cin 2610  c0 2726  csn 2803  1cc1c 3238   Nn cnnc 3481   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