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

Theorem omex 8011
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 7989.

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 6647 and  Fin  =  _V (the universe of all sets) by fineqv 7688. 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 6655 through peano5 6659 (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 8010 . 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 2791 . . . 4  |-  ( A. y  e.  x  suc  y  e.  x  ->  A. y  e.  om  (
y  e.  x  ->  suc  y  e.  x
) )
4 peano5 6659 . . . 4  |-  ( (
(/)  e.  x  /\  A. y  e.  om  (
y  e.  x  ->  suc  y  e.  x
) )  ->  om  C_  x
)
53, 4sylan2 472 . . 3  |-  ( (
(/)  e.  x  /\  A. y  e.  x  suc  y  e.  x )  ->  om  C_  x )
65eximi 1675 . 2  |-  ( E. x ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
)  ->  E. x om  C_  x )
7 vex 3059 . . . 4  |-  x  e. 
_V
87ssex 4535 . . 3  |-  ( om  C_  x  ->  om  e.  _V )
98exlimiv 1741 . 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 367   E.wex 1631    e. wcel 1840   A.wral 2751   _Vcvv 3056    C_ wss 3411   (/)c0 3735   suc csuc 4821   omcom 6636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-8 1842  ax-9 1844  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378  ax-sep 4514  ax-nul 4522  ax-pr 4627  ax-un 6528  ax-inf2 8009
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 973  df-3an 974  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-eu 2240  df-mo 2241  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ne 2598  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3058  df-sbc 3275  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-pss 3427  df-nul 3736  df-if 3883  df-pw 3954  df-sn 3970  df-pr 3972  df-tp 3974  df-op 3976  df-uni 4189  df-br 4393  df-opab 4451  df-tr 4487  df-eprel 4731  df-po 4741  df-so 4742  df-fr 4779  df-we 4781  df-ord 4822  df-on 4823  df-lim 4824  df-suc 4825  df-om 6637
This theorem is referenced by:  axinf  8012  inf5  8013  omelon  8014  dfom3  8015  elom3  8016  oancom  8019  isfinite  8020  nnsdom  8021  omenps  8022  omensuc  8023  unbnn3  8026  noinfep  8027  tz9.1  8110  tz9.1c  8111  fseqdom  8357  fseqen  8358  aleph0  8397  alephprc  8430  alephfplem1  8435  alephfplem4  8438  iunfictbso  8445  unctb  8535  r1om  8574  cfom  8594  itunifval  8746  hsmexlem5  8760  axcc2lem  8766  acncc  8770  axcc4dom  8771  domtriomlem  8772  axdclem2  8850  infinf  8891  unirnfdomd  8892  alephval2  8897  dominfac  8898  iunctb  8899  pwfseqlem4  8988  pwfseqlem5  8989  pwxpndom2  8991  pwcdandom  8993  gchac  9007  wunex2  9064  tskinf  9095  niex  9207  nnexALT  10496  ltweuz  12024  uzenom  12027  nnenom  12042  axdc4uzlem  12044  seqex  12061  rexpen  14060  cctop  19689  2ndcctbss  20138  2ndcdisj  20139  2ndcdisj2  20140  tx1stc  20333  tx2ndc  20334  met2ndci  21207  xpct  27860  snct  27861  fnct  27863  bnj852  29182  bnj865  29184  trpredex  29988
  Copyright terms: Public domain W3C validator