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

Theorem omex 8060
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 8038.

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 6695 and  Fin  =  _V (the universe of all sets) by fineqv 7735. 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 6703 through peano5 6707 (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 8059 . 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 2854 . . . 4  |-  ( A. y  e.  x  suc  y  e.  x  ->  A. y  e.  om  (
y  e.  x  ->  suc  y  e.  x
) )
4 peano5 6707 . . . 4  |-  ( (
(/)  e.  x  /\  A. y  e.  om  (
y  e.  x  ->  suc  y  e.  x
) )  ->  om  C_  x
)
53, 4sylan2 474 . . 3  |-  ( (
(/)  e.  x  /\  A. y  e.  x  suc  y  e.  x )  ->  om  C_  x )
65eximi 1635 . 2  |-  ( E. x ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
)  ->  E. x om  C_  x )
7 vex 3116 . . . 4  |-  x  e. 
_V
87ssex 4591 . . 3  |-  ( om  C_  x  ->  om  e.  _V )
98exlimiv 1698 . 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 369   E.wex 1596    e. wcel 1767   A.wral 2814   _Vcvv 3113    C_ wss 3476   (/)c0 3785   suc csuc 4880   omcom 6684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686  ax-un 6576  ax-inf2 8058
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-tr 4541  df-eprel 4791  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-om 6685
This theorem is referenced by:  axinf  8061  inf5  8062  omelon  8063  dfom3  8064  elom3  8065  oancom  8068  isfinite  8069  nnsdom  8070  omenps  8071  omensuc  8072  unbnn3  8075  noinfep  8076  noinfepOLD  8077  tz9.1  8160  tz9.1c  8161  fseqdom  8407  fseqen  8408  aleph0  8447  alephprc  8480  alephfplem1  8485  alephfplem4  8488  iunfictbso  8495  unctb  8585  r1om  8624  cfom  8644  itunifval  8796  hsmexlem5  8810  axcc2lem  8816  acncc  8820  axcc4dom  8821  domtriomlem  8822  axdclem2  8900  infinf  8941  unirnfdomd  8942  alephval2  8947  dominfac  8948  iunctb  8949  pwfseqlem4  9040  pwfseqlem5  9041  pwxpndom2  9043  pwcdandom  9045  gchac  9059  wunex2  9116  tskinf  9147  niex  9259  nnexALT  10538  ltweuz  12040  uzenom  12043  nnenom  12058  axdc4uzlem  12060  seqex  12077  rexpen  13822  cctop  19301  2ndcctbss  19750  2ndcdisj  19751  2ndcdisj2  19752  tx1stc  19914  tx2ndc  19915  met2ndci  20788  xpct  27233  snct  27234  fnct  27236  trpredex  28925  bnj852  33076  bnj865  33078
  Copyright terms: Public domain W3C validator