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

Theorem omex 7298
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 7276.

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 4625 and  Fin  =  _V (the universe of all sets) by fineqv 7032. 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 4633 through peano5 4637 (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
StepHypRef Expression
1 zfinf2 7297 . 2  |-  E. x
( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x )
2 ax-1 7 . . . . 5  |-  ( ( y  e.  x  ->  suc  y  e.  x
)  ->  ( y  e.  om  ->  ( y  e.  x  ->  suc  y  e.  x ) ) )
32ralimi2 2588 . . . 4  |-  ( A. y  e.  x  suc  y  e.  x  ->  A. y  e.  om  (
y  e.  x  ->  suc  y  e.  x
) )
4 peano5 4637 . . . 4  |-  ( (
(/)  e.  x  /\  A. y  e.  om  (
y  e.  x  ->  suc  y  e.  x
) )  ->  om  C_  x
)
53, 4sylan2 462 . . 3  |-  ( (
(/)  e.  x  /\  A. y  e.  x  suc  y  e.  x )  ->  om  C_  x )
65eximi 1574 . 2  |-  ( E. x ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
)  ->  E. x om  C_  x )
7 vex 2760 . . . 4  |-  x  e. 
_V
87ssex 4118 . . 3  |-  ( om  C_  x  ->  om  e.  _V )
98exlimiv 2024 . 2  |-  ( E. x om  C_  x  ->  om  e.  _V )
101, 6, 9mp2b 11 1  |-  om  e.  _V
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360   E.wex 1537    e. wcel 1621   A.wral 2516   _Vcvv 2757    C_ wss 3113   (/)c0 3416   suc csuc 4352   omcom 4614
This theorem is referenced by:  axinf  7299  inf5  7300  omelon  7301  dfom3  7302  elom3  7303  oancom  7306  isfinite  7307  nnsdom  7308  omenps  7309  omensuc  7310  unbnn3  7313  noinfep  7314  noinfepOLD  7315  tz9.1  7365  tz9.1c  7366  fseqdom  7607  fseqen  7608  aleph0  7647  alephprc  7680  alephfplem1  7685  alephfplem4  7688  iunfictbso  7695  unctb  7785  r1om  7824  cfom  7844  itunifval  7996  hsmexlem5  8010  axcc2lem  8016  acncc  8020  axcc4dom  8021  domtriomlem  8022  axdclem2  8101  infinf  8142  unirnfdomd  8143  alephval2  8148  dominfac  8149  iunctb  8150  pwfseqlem4  8238  pwfseqlem5  8239  pwxpndom2  8241  pwcdandom  8243  gchac  8249  wunex2  8314  tskinf  8345  niex  8459  nnexALT  9702  ltweuz  10976  uzenom  10979  nnenom  10994  axdc4uzlem  10996  seqex  11000  rexpen  12454  cctop  16691  2ndcctbss  17129  2ndcdisj  17130  2ndcdisj2  17131  tx1stc  17292  tx2ndc  17293  met2ndci  18016  trpredex  23595  trclval  25247  cartarlim  25258  bnj852  27986  bnj865  27988
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pr 4172  ax-un 4470  ax-inf2 7296
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-sbc 2953  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-pss 3129  df-nul 3417  df-if 3526  df-pw 3587  df-sn 3606  df-pr 3607  df-tp 3608  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-tr 4074  df-eprel 4263  df-po 4272  df-so 4273  df-fr 4310  df-we 4312  df-ord 4353  df-on 4354  df-lim 4355  df-suc 4356  df-om 4615
  Copyright terms: Public domain W3C validator