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

Theorem omex 8063
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 8041.

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 6696 and  Fin  =  _V (the universe of all sets) by fineqv 7737. 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 6704 through peano5 6708 (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 8062 . 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 2833 . . . 4  |-  ( A. y  e.  x  suc  y  e.  x  ->  A. y  e.  om  (
y  e.  x  ->  suc  y  e.  x
) )
4 peano5 6708 . . . 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 1643 . 2  |-  ( E. x ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
)  ->  E. x om  C_  x )
7 vex 3098 . . . 4  |-  x  e. 
_V
87ssex 4581 . . 3  |-  ( om  C_  x  ->  om  e.  _V )
98exlimiv 1709 . 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 1599    e. wcel 1804   A.wral 2793   _Vcvv 3095    C_ wss 3461   (/)c0 3770   suc csuc 4870   omcom 6685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676  ax-un 6577  ax-inf2 8061
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-tr 4531  df-eprel 4781  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-om 6686
This theorem is referenced by:  axinf  8064  inf5  8065  omelon  8066  dfom3  8067  elom3  8068  oancom  8071  isfinite  8072  nnsdom  8073  omenps  8074  omensuc  8075  unbnn3  8078  noinfep  8079  noinfepOLD  8080  tz9.1  8163  tz9.1c  8164  fseqdom  8410  fseqen  8411  aleph0  8450  alephprc  8483  alephfplem1  8488  alephfplem4  8491  iunfictbso  8498  unctb  8588  r1om  8627  cfom  8647  itunifval  8799  hsmexlem5  8813  axcc2lem  8819  acncc  8823  axcc4dom  8824  domtriomlem  8825  axdclem2  8903  infinf  8944  unirnfdomd  8945  alephval2  8950  dominfac  8951  iunctb  8952  pwfseqlem4  9043  pwfseqlem5  9044  pwxpndom2  9046  pwcdandom  9048  gchac  9062  wunex2  9119  tskinf  9150  niex  9262  nnexALT  10545  ltweuz  12054  uzenom  12057  nnenom  12072  axdc4uzlem  12074  seqex  12091  rexpen  13943  cctop  19485  2ndcctbss  19934  2ndcdisj  19935  2ndcdisj2  19936  tx1stc  20129  tx2ndc  20130  met2ndci  21003  xpct  27511  snct  27512  fnct  27514  trpredex  29296  bnj852  33847  bnj865  33849
  Copyright terms: Public domain W3C validator