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 7224 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 7233 through peano5 7237 (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 3098 . . . 4 (∀𝑦𝑥 suc 𝑦𝑥 → ∀𝑦 ∈ ω (𝑦𝑥 → suc 𝑦𝑥))
4 peano5 7237 . . . 4 ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦𝑥 → suc 𝑦𝑥)) → ω ⊆ 𝑥)
53, 4sylan2 574 . . 3 ((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ω ⊆ 𝑥)
65eximi 1910 . 2 (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ∃𝑥ω ⊆ 𝑥)
7 vex 3354 . . . 4 𝑥 ∈ V
87ssex 4937 . . 3 (ω ⊆ 𝑥 → ω ∈ V)
98exlimiv 2010 . 2 (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
101, 6, 9mp2b 10 1 ω ∈ V
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wex 1852  wcel 2145  wral 3061  Vcvv 3351  wss 3724  c0 4064  suc csuc 5869  ωcom 7213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035  ax-un 7097  ax-inf2 8703
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3589  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-tr 4888  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-om 7214
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  9040  fseqdom  9050  fseqen  9051  aleph0  9090  alephprc  9123  alephfplem1  9128  alephfplem4  9131  iunfictbso  9138  unctb  9230  r1om  9269  cfom  9289  itunifval  9441  hsmexlem5  9455  axcc2lem  9461  acncc  9465  axcc4dom  9466  domtriomlem  9467  axdclem2  9545  fnct  9562  infinf  9591  unirnfdomd  9592  alephval2  9597  dominfac  9598  iunctb  9599  pwfseqlem4  9687  pwfseqlem5  9688  pwxpndom2  9690  pwcdandom  9692  gchac  9706  wunex2  9763  tskinf  9794  niex  9906  nnexALT  11225  ltweuz  12969  uzenom  12972  nnenom  12988  axdc4uzlem  12991  seqex  13011  rexpen  15164  cctop  21032  2ndcctbss  21480  2ndcdisj  21481  2ndcdisj2  21482  tx1stc  21675  tx2ndc  21676  met2ndci  22548  snct  29832  bnj852  31330  bnj865  31332  trpredex  32074
  Copyright terms: Public domain W3C validator