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

Theorem omex 8400
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 8378.

A finitist (someone who doesn't believe in infinity) could, without contradiction, replace the Axiom of Infinity by its denial ¬ ω ∈ V; this would lead to ω = On by omon 6945 and Fin = V (the universe of all sets) by fineqv 8037. 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 6954 through peano5 6958 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.)

Assertion
Ref Expression
omex ω ∈ V

Proof of Theorem omex
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zfinf2 8399 . 2 𝑥(∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)
2 ax-1 6 . . . . 5 ((𝑦𝑥 → suc 𝑦𝑥) → (𝑦 ∈ ω → (𝑦𝑥 → suc 𝑦𝑥)))
32ralimi2 2932 . . . 4 (∀𝑦𝑥 suc 𝑦𝑥 → ∀𝑦 ∈ ω (𝑦𝑥 → suc 𝑦𝑥))
4 peano5 6958 . . . 4 ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦𝑥 → suc 𝑦𝑥)) → ω ⊆ 𝑥)
53, 4sylan2 489 . . 3 ((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ω ⊆ 𝑥)
65eximi 1751 . 2 (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ∃𝑥ω ⊆ 𝑥)
7 vex 3175 . . . 4 𝑥 ∈ V
87ssex 4725 . . 3 (ω ⊆ 𝑥 → ω ∈ V)
98exlimiv 1844 . 2 (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
101, 6, 9mp2b 10 1 ω ∈ V
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wex 1694  wcel 1976  wral 2895  Vcvv 3172  wss 3539  c0 3873  suc csuc 5628  ωcom 6934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828  ax-un 6824  ax-inf2 8398
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-tr 4675  df-eprel 4939  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-om 6935
This theorem is referenced by:  axinf  8401  inf5  8402  omelon  8403  dfom3  8404  elom3  8405  oancom  8408  isfinite  8409  nnsdom  8411  omenps  8412  omensuc  8413  unbnn3  8416  noinfep  8417  tz9.1  8465  tz9.1c  8466  xpct  8699  fseqdom  8709  fseqen  8710  aleph0  8749  alephprc  8782  alephfplem1  8787  alephfplem4  8790  iunfictbso  8797  unctb  8887  r1om  8926  cfom  8946  itunifval  9098  hsmexlem5  9112  axcc2lem  9118  acncc  9122  axcc4dom  9123  domtriomlem  9124  axdclem2  9202  infinf  9244  unirnfdomd  9245  alephval2  9250  dominfac  9251  iunctb  9252  pwfseqlem4  9340  pwfseqlem5  9341  pwxpndom2  9343  pwcdandom  9345  gchac  9359  wunex2  9416  tskinf  9447  niex  9559  nnexALT  10869  ltweuz  12577  uzenom  12580  nnenom  12596  axdc4uzlem  12599  seqex  12620  rexpen  14742  cctop  20562  2ndcctbss  21010  2ndcdisj  21011  2ndcdisj2  21012  tx1stc  21205  tx2ndc  21206  met2ndci  22078  snct  28680  fnct  28682  bnj852  30051  bnj865  30053  trpredex  30787
  Copyright terms: Public domain W3C validator