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

Theorem omex 7225
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 7203.

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 4555 and  Fin  =  _V (the universe of all sets) by fineqv 6960. 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 4563 through peano5 4567 (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 7224 . 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 2575 . . . 4  |-  ( A. y  e.  x  suc  y  e.  x  ->  A. y  e.  om  (
y  e.  x  ->  suc  y  e.  x
) )
4 peano5 4567 . . . 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 2728 . . . 4  |-  x  e. 
_V
87ssex 4052 . . 3  |-  ( om  C_  x  ->  om  e.  _V )
98exlimiv 2023 . 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 2507   _Vcvv 2725    C_ wss 3075   (/)c0 3359   suc csuc 4284   omcom 4544
This theorem is referenced by:  axinf  7226  inf5  7227  omelon  7228  dfom3  7229  elom3  7230  oancom  7233  isfinite  7234  nnsdom  7235  omenps  7236  omensuc  7237  unbnn3  7240  noinfep  7241  noinfepOLD  7242  tz9.1  7292  tz9.1c  7293  fseqdom  7534  fseqen  7535  aleph0  7574  alephprc  7607  alephfplem1  7612  alephfplem4  7615  iunfictbso  7622  unctb  7712  r1om  7751  cfom  7771  itunifval  7923  hsmexlem5  7937  axcc2lem  7943  acncc  7947  axcc4dom  7948  domtriomlem  7949  axdclem2  8028  alephval2  8071  dominfac  8072  iunctb  8073  pwfseqlem4  8161  pwfseqlem5  8162  pwxpndom2  8164  pwcdandom  8166  gchac  8172  wunex2  8237  tskinf  8268  niex  8382  nnexALT  9596  ltweuz  10867  uzenom  10870  nnenom  10885  axdc4uzlem  10887  seqex  10891  rexpen  12342  cctop  16537  2ndcctbss  16975  2ndcdisj  16976  2ndcdisj2  16977  tx1stc  17138  tx2ndc  17139  met2ndci  17862  trpredex  23337  trclval  24989  cartarlim  25000  bnj852  27580  bnj865  27582
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 1926  ax-ext 2234  ax-sep 4035  ax-nul 4043  ax-pr 4105  ax-un 4400  ax-inf2 7223
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 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2511  df-rex 2512  df-rab 2514  df-v 2727  df-sbc 2920  df-dif 3078  df-un 3080  df-in 3082  df-ss 3086  df-pss 3088  df-nul 3360  df-if 3468  df-pw 3529  df-sn 3547  df-pr 3548  df-tp 3549  df-op 3550  df-uni 3725  df-br 3918  df-opab 3972  df-tr 4008  df-eprel 4195  df-po 4204  df-so 4205  df-fr 4242  df-we 4244  df-ord 4285  df-on 4286  df-lim 4287  df-suc 4288  df-om 4545
  Copyright terms: Public domain W3C validator