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

Theorem omex 8094
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 8072.

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 6654 and  Fin  =  _V (the universe of all sets) by fineqv 7733. 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 6663 through peano5 6667 (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 8093 . 2  |-  E. x
( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x )
2 ax-1 6 . . . . 5  |-  ( ( y  e.  x  ->  suc  y  e.  x
)  ->  ( y  e.  om  ->  ( y  e.  x  ->  suc  y  e.  x ) ) )
32ralimi2 2749 . . . 4  |-  ( A. y  e.  x  suc  y  e.  x  ->  A. y  e.  om  (
y  e.  x  ->  suc  y  e.  x
) )
4 peano5 6667 . . . 4  |-  ( (
(/)  e.  x  /\  A. y  e.  om  (
y  e.  x  ->  suc  y  e.  x
) )  ->  om  C_  x
)
53, 4sylan2 476 . . 3  |-  ( (
(/)  e.  x  /\  A. y  e.  x  suc  y  e.  x )  ->  om  C_  x )
65eximi 1701 . 2  |-  ( E. x ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
)  ->  E. x om  C_  x )
7 vex 3019 . . . 4  |-  x  e. 
_V
87ssex 4504 . . 3  |-  ( om  C_  x  ->  om  e.  _V )
98exlimiv 1770 . 2  |-  ( E. x om  C_  x  ->  om  e.  _V )
101, 6, 9mp2b 10 1  |-  om  e.  _V
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   E.wex 1657    e. wcel 1872   A.wral 2708   _Vcvv 3016    C_ wss 3372   (/)c0 3697   suc csuc 5380   omcom 6643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-sep 4482  ax-nul 4491  ax-pr 4596  ax-un 6534  ax-inf2 8092
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-ral 2713  df-rex 2714  df-rab 2717  df-v 3018  df-sbc 3236  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-tp 3939  df-op 3941  df-uni 4156  df-br 4360  df-opab 4419  df-tr 4455  df-eprel 4700  df-po 4710  df-so 4711  df-fr 4748  df-we 4750  df-ord 5381  df-on 5382  df-lim 5383  df-suc 5384  df-om 6644
This theorem is referenced by:  axinf  8095  inf5  8096  omelon  8097  dfom3  8098  elom3  8099  oancom  8102  isfinite  8103  nnsdom  8104  omenps  8105  omensuc  8106  unbnn3  8109  noinfep  8110  tz9.1  8158  tz9.1c  8159  fseqdom  8401  fseqen  8402  aleph0  8441  alephprc  8474  alephfplem1  8479  alephfplem4  8482  iunfictbso  8489  unctb  8579  r1om  8618  cfom  8638  itunifval  8790  hsmexlem5  8804  axcc2lem  8810  acncc  8814  axcc4dom  8815  domtriomlem  8816  axdclem2  8894  infinf  8935  unirnfdomd  8936  alephval2  8941  dominfac  8942  iunctb  8943  pwfseqlem4  9031  pwfseqlem5  9032  pwxpndom2  9034  pwcdandom  9036  gchac  9050  wunex2  9107  tskinf  9138  niex  9250  nnexALT  10555  ltweuz  12118  uzenom  12121  nnenom  12136  axdc4uzlem  12138  seqex  12158  rexpen  14216  cctop  19956  2ndcctbss  20405  2ndcdisj  20406  2ndcdisj2  20407  tx1stc  20600  tx2ndc  20601  met2ndci  21472  xpct  28237  snct  28238  fnct  28240  bnj852  29677  bnj865  29679  trpredex  30422
  Copyright terms: Public domain W3C validator