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

Theorem omex 7228
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 7206.

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 4558 and  Fin  =  _V (the universe of all sets) by fineqv 6963. 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 4566 through peano5 4570 (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 7227 . 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 2577 . . . 4  |-  ( A. y  e.  x  suc  y  e.  x  ->  A. y  e.  om  (
y  e.  x  ->  suc  y  e.  x
) )
4 peano5 4570 . . . 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 2730 . . . 4  |-  x  e. 
_V
87ssex 4055 . . 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 2509   _Vcvv 2727    C_ wss 3078   (/)c0 3362   suc csuc 4287   omcom 4547
This theorem is referenced by:  axinf  7229  inf5  7230  omelon  7231  dfom3  7232  elom3  7233  oancom  7236  isfinite  7237  nnsdom  7238  omenps  7239  omensuc  7240  unbnn3  7243  noinfep  7244  noinfepOLD  7245  tz9.1  7295  tz9.1c  7296  fseqdom  7537  fseqen  7538  aleph0  7577  alephprc  7610  alephfplem1  7615  alephfplem4  7618  iunfictbso  7625  unctb  7715  r1om  7754  cfom  7774  itunifval  7926  hsmexlem5  7940  axcc2lem  7946  acncc  7950  axcc4dom  7951  domtriomlem  7952  axdclem2  8031  alephval2  8074  dominfac  8075  iunctb  8076  pwfseqlem4  8164  pwfseqlem5  8165  pwxpndom2  8167  pwcdandom  8169  gchac  8175  wunex2  8240  tskinf  8271  niex  8385  nnexALT  9628  ltweuz  10902  uzenom  10905  nnenom  10920  axdc4uzlem  10922  seqex  10926  rexpen  12380  cctop  16575  2ndcctbss  17013  2ndcdisj  17014  2ndcdisj2  17015  tx1stc  17176  tx2ndc  17177  met2ndci  17900  trpredex  23408  trclval  25060  cartarlim  25071  bnj852  27739  bnj865  27741
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 4038  ax-nul 4046  ax-pr 4108  ax-un 4403  ax-inf2 7226
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 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-pss 3091  df-nul 3363  df-if 3471  df-pw 3532  df-sn 3550  df-pr 3551  df-tp 3552  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-tr 4011  df-eprel 4198  df-po 4207  df-so 4208  df-fr 4245  df-we 4247  df-ord 4288  df-on 4289  df-lim 4290  df-suc 4291  df-om 4548
  Copyright terms: Public domain W3C validator