MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  omex Unicode version

Theorem omex 7554
Description: The existence of omega (the class of natural numbers). Axiom 7 of [TakeutiZaring] p. 43. This theorem is proved assuming the Axiom of Infinity and in fact is equivalent to it, as shown by the reverse derivation inf0 7532.

A finitist (someone who doesn't believe in infinity) could, without contradiction, replace the Axiom of Infinity by its denial  -.  om  e.  _V; this would lead to  om  =  On by omon 4815 and  Fin  =  _V (the universe of all sets) by fineqv 7283. The finitist could still develop natural number, integer, and rational number arithmetic but would be denied the real numbers (as well as much of the rest of mathematics). In deference to the finitist, much of our development is done, when possible, without invoking the Axiom of Infinity; an example is Peano's axioms peano1 4823 through peano5 4827 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.)

Assertion
Ref Expression
omex  |-  om  e.  _V

Proof of Theorem omex
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zfinf2 7553 . 2  |-  E. x
( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x )
2 ax-1 5 . . . . 5  |-  ( ( y  e.  x  ->  suc  y  e.  x
)  ->  ( y  e.  om  ->  ( y  e.  x  ->  suc  y  e.  x ) ) )
32ralimi2 2738 . . . 4  |-  ( A. y  e.  x  suc  y  e.  x  ->  A. y  e.  om  (
y  e.  x  ->  suc  y  e.  x
) )
4 peano5 4827 . . . 4  |-  ( (
(/)  e.  x  /\  A. y  e.  om  (
y  e.  x  ->  suc  y  e.  x
) )  ->  om  C_  x
)
53, 4sylan2 461 . . 3  |-  ( (
(/)  e.  x  /\  A. y  e.  x  suc  y  e.  x )  ->  om  C_  x )
65eximi 1582 . 2  |-  ( E. x ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
)  ->  E. x om  C_  x )
7 vex 2919 . . . 4  |-  x  e. 
_V
87ssex 4307 . . 3  |-  ( om  C_  x  ->  om  e.  _V )
98exlimiv 1641 . 2  |-  ( E. x om  C_  x  ->  om  e.  _V )
101, 6, 9mp2b 10 1  |-  om  e.  _V
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   E.wex 1547    e. wcel 1721   A.wral 2666   _Vcvv 2916    C_ wss 3280   (/)c0 3588   suc csuc 4543   omcom 4804
This theorem is referenced by:  axinf  7555  inf5  7556  omelon  7557  dfom3  7558  elom3  7559  oancom  7562  isfinite  7563  nnsdom  7564  omenps  7565  omensuc  7566  unbnn3  7569  noinfep  7570  noinfepOLD  7571  tz9.1  7621  tz9.1c  7622  fseqdom  7863  fseqen  7864  aleph0  7903  alephprc  7936  alephfplem1  7941  alephfplem4  7944  iunfictbso  7951  unctb  8041  r1om  8080  cfom  8100  itunifval  8252  hsmexlem5  8266  axcc2lem  8272  acncc  8276  axcc4dom  8277  domtriomlem  8278  axdclem2  8356  infinf  8397  unirnfdomd  8398  alephval2  8403  dominfac  8404  iunctb  8405  pwfseqlem4  8493  pwfseqlem5  8494  pwxpndom2  8496  pwcdandom  8498  gchac  8504  wunex2  8569  tskinf  8600  niex  8714  nnexALT  9958  ltweuz  11256  uzenom  11259  nnenom  11274  axdc4uzlem  11276  seqex  11280  rexpen  12782  cctop  17025  2ndcctbss  17471  2ndcdisj  17472  2ndcdisj2  17473  tx1stc  17635  tx2ndc  17636  met2ndci  18505  xpct  24055  snct  24056  fnct  24058  trpredex  25454  bnj852  28998  bnj865  29000
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363  ax-un 4660  ax-inf2 7552
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-tr 4263  df-eprel 4454  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805
  Copyright terms: Public domain W3C validator