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

Theorem omex 8233
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 8211.

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 6780 and Fin = V (the universe of all sets) by fineqv 7871. 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 6789 through peano5 6793 (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 8232 . 2 𝑥(∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)
2 ax-1 6 . . . . 5 ((𝑦𝑥 → suc 𝑦𝑥) → (𝑦 ∈ ω → (𝑦𝑥 → suc 𝑦𝑥)))
32ralimi2 2828 . . . 4 (∀𝑦𝑥 suc 𝑦𝑥 → ∀𝑦 ∈ ω (𝑦𝑥 → suc 𝑦𝑥))
4 peano5 6793 . . . 4 ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦𝑥 → suc 𝑦𝑥)) → ω ⊆ 𝑥)
53, 4sylan2 484 . . 3 ((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ω ⊆ 𝑥)
65eximi 1738 . 2 (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ∃𝑥ω ⊆ 𝑥)
7 vex 3069 . . . 4 𝑥 ∈ V
87ssex 4580 . . 3 (ω ⊆ 𝑥 → ω ∈ V)
98exlimiv 1807 . 2 (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
101, 6, 9mp2b 10 1 ω ∈ V
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 378  wex 1692  wcel 1937  wral 2791  Vcvv 3066  wss 3426  c0 3757  suc csuc 5476  ωcom 6769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680  ax-un 6659  ax-inf2 8231
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-sbc 3292  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-br 4435  df-opab 4494  df-tr 4531  df-eprel 4791  df-po 4801  df-so 4802  df-fr 4839  df-we 4841  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-om 6770
This theorem is referenced by:  axinf  8234  inf5  8235  omelon  8236  dfom3  8237  elom3  8238  oancom  8241  isfinite  8242  nnsdom  8244  omenps  8245  omensuc  8246  unbnn3  8249  noinfep  8250  tz9.1  8298  tz9.1c  8299  xpct  8532  fseqdom  8542  fseqen  8543  aleph0  8582  alephprc  8615  alephfplem1  8620  alephfplem4  8623  iunfictbso  8630  unctb  8720  r1om  8759  cfom  8779  itunifval  8931  hsmexlem5  8945  axcc2lem  8951  acncc  8955  axcc4dom  8956  domtriomlem  8957  axdclem2  9035  infinf  9076  unirnfdomd  9077  alephval2  9082  dominfac  9083  iunctb  9084  pwfseqlem4  9172  pwfseqlem5  9173  pwxpndom2  9175  pwcdandom  9177  gchac  9191  wunex2  9248  tskinf  9279  niex  9391  nnexALT  10700  ltweuz  12288  uzenom  12291  nnenom  12306  axdc4uzlem  12309  seqex  12329  rexpen  14440  cctop  20178  2ndcctbss  20627  2ndcdisj  20628  2ndcdisj2  20629  tx1stc  20822  tx2ndc  20823  met2ndci  21695  snct  28451  fnct  28453  bnj852  29884  bnj865  29886  trpredex  30629
  Copyright terms: Public domain W3C validator