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

Theorem omex 8705
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 8683.

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 7233 and Fin = V (the universe of all sets) by fineqv 8332. 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 7242 through peano5 7246 (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 8704 . 2 𝑥(∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)
2 ax-1 6 . . . . 5 ((𝑦𝑥 → suc 𝑦𝑥) → (𝑦 ∈ ω → (𝑦𝑥 → suc 𝑦𝑥)))
32ralimi2 3079 . . . 4 (∀𝑦𝑥 suc 𝑦𝑥 → ∀𝑦 ∈ ω (𝑦𝑥 → suc 𝑦𝑥))
4 peano5 7246 . . . 4 ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦𝑥 → suc 𝑦𝑥)) → ω ⊆ 𝑥)
53, 4sylan2 492 . . 3 ((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ω ⊆ 𝑥)
65eximi 1903 . 2 (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ∃𝑥ω ⊆ 𝑥)
7 vex 3335 . . . 4 𝑥 ∈ V
87ssex 4946 . . 3 (ω ⊆ 𝑥 → ω ∈ V)
98exlimiv 1999 . 2 (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
101, 6, 9mp2b 10 1 ω ∈ V
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wex 1845  wcel 2131  wral 3042  Vcvv 3332  wss 3707  c0 4050  suc csuc 5878  ωcom 7222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047  ax-un 7106  ax-inf2 8703
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-tr 4897  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-we 5219  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-om 7223
This theorem is referenced by:  axinf  8706  inf5  8707  omelon  8708  dfom3  8709  elom3  8710  oancom  8713  isfinite  8714  nnsdom  8716  omenps  8717  omensuc  8718  unbnn3  8721  noinfep  8722  tz9.1  8770  tz9.1c  8771  xpct  9021  fseqdom  9031  fseqen  9032  aleph0  9071  alephprc  9104  alephfplem1  9109  alephfplem4  9112  iunfictbso  9119  unctb  9211  r1om  9250  cfom  9270  itunifval  9422  hsmexlem5  9436  axcc2lem  9442  acncc  9446  axcc4dom  9447  domtriomlem  9448  axdclem2  9526  fnct  9543  infinf  9572  unirnfdomd  9573  alephval2  9578  dominfac  9579  iunctb  9580  pwfseqlem4  9668  pwfseqlem5  9669  pwxpndom2  9671  pwcdandom  9673  gchac  9687  wunex2  9744  tskinf  9775  niex  9887  nnexALT  11206  ltweuz  12946  uzenom  12949  nnenom  12965  axdc4uzlem  12968  seqex  12989  rexpen  15148  cctop  21004  2ndcctbss  21452  2ndcdisj  21453  2ndcdisj2  21454  tx1stc  21647  tx2ndc  21648  met2ndci  22520  snct  29792  bnj852  31290  bnj865  31292  trpredex  32034
  Copyright terms: Public domain W3C validator