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

Theorem omex 8298
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 8276.

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 6843 and Fin = V (the universe of all sets) by fineqv 7935. 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 6852 through peano5 6856 (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 8297 . 2 𝑥(∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)
2 ax-1 6 . . . . 5 ((𝑦𝑥 → suc 𝑦𝑥) → (𝑦 ∈ ω → (𝑦𝑥 → suc 𝑦𝑥)))
32ralimi2 2837 . . . 4 (∀𝑦𝑥 suc 𝑦𝑥 → ∀𝑦 ∈ ω (𝑦𝑥 → suc 𝑦𝑥))
4 peano5 6856 . . . 4 ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦𝑥 → suc 𝑦𝑥)) → ω ⊆ 𝑥)
53, 4sylan2 489 . . 3 ((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ω ⊆ 𝑥)
65eximi 1740 . 2 (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ∃𝑥ω ⊆ 𝑥)
7 vex 3080 . . . 4 𝑥 ∈ V
87ssex 4629 . . 3 (ω ⊆ 𝑥 → ω ∈ V)
98exlimiv 1811 . 2 (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
101, 6, 9mp2b 10 1 ω ∈ V
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wex 1694  wcel 1938  wral 2800  Vcvv 3077  wss 3444  c0 3777  suc csuc 5532  ωcom 6832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732  ax-un 6722  ax-inf2 8296
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 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-tr 4579  df-eprel 4843  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-om 6833
This theorem is referenced by:  axinf  8299  inf5  8300  omelon  8301  dfom3  8302  elom3  8303  oancom  8306  isfinite  8307  nnsdom  8309  omenps  8310  omensuc  8311  unbnn3  8314  noinfep  8315  tz9.1  8363  tz9.1c  8364  xpct  8597  fseqdom  8607  fseqen  8608  aleph0  8647  alephprc  8680  alephfplem1  8685  alephfplem4  8688  iunfictbso  8695  unctb  8785  r1om  8824  cfom  8844  itunifval  8996  hsmexlem5  9010  axcc2lem  9016  acncc  9020  axcc4dom  9021  domtriomlem  9022  axdclem2  9100  infinf  9142  unirnfdomd  9143  alephval2  9148  dominfac  9149  iunctb  9150  pwfseqlem4  9238  pwfseqlem5  9239  pwxpndom2  9241  pwcdandom  9243  gchac  9257  wunex2  9314  tskinf  9345  niex  9457  nnexALT  10776  ltweuz  12489  uzenom  12492  nnenom  12508  axdc4uzlem  12511  seqex  12532  rexpen  14663  cctop  20521  2ndcctbss  20969  2ndcdisj  20970  2ndcdisj2  20971  tx1stc  21164  tx2ndc  21165  met2ndci  22037  snct  28663  fnct  28665  bnj852  30091  bnj865  30093  trpredex  30824
  Copyright terms: Public domain W3C validator