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

Theorem omex 9108
 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 9086. 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 7593 and Fin = V (the universe of all sets) by fineqv 8735. 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 7603 through peano5 7607 (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 9107 . 2 𝑥(∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)
2 ax-1 6 . . . . 5 ((𝑦𝑥 → suc 𝑦𝑥) → (𝑦 ∈ ω → (𝑦𝑥 → suc 𝑦𝑥)))
32ralimi2 3159 . . . 4 (∀𝑦𝑥 suc 𝑦𝑥 → ∀𝑦 ∈ ω (𝑦𝑥 → suc 𝑦𝑥))
4 peano5 7607 . . . 4 ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦𝑥 → suc 𝑦𝑥)) → ω ⊆ 𝑥)
53, 4sylan2 594 . . 3 ((∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ω ⊆ 𝑥)
65eximi 1835 . 2 (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥) → ∃𝑥ω ⊆ 𝑥)
7 vex 3499 . . . 4 𝑥 ∈ V
87ssex 5227 . . 3 (ω ⊆ 𝑥 → ω ∈ V)
98exlimiv 1931 . 2 (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
101, 6, 9mp2b 10 1 ω ∈ V
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  ∀wral 3140  Vcvv 3496   ⊆ wss 3938  ∅c0 4293  suc csuc 6195  ωcom 7582 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332  ax-un 7463  ax-inf2 9106 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-tr 5175  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-om 7583 This theorem is referenced by:  axinf  9109  inf5  9110  omelon  9111  dfom3  9112  elom3  9113  oancom  9116  isfinite  9117  nnsdom  9119  omenps  9120  omensuc  9121  unbnn3  9124  noinfep  9125  tz9.1  9173  tz9.1c  9174  xpct  9444  fseqdom  9454  fseqen  9455  aleph0  9494  alephprc  9527  alephfplem1  9532  alephfplem4  9535  iunfictbso  9542  unctb  9629  r1om  9668  cfom  9688  itunifval  9840  hsmexlem5  9854  axcc2lem  9860  acncc  9864  axcc4dom  9865  domtriomlem  9866  axdclem2  9944  fnct  9961  infinf  9990  unirnfdomd  9991  alephval2  9996  dominfac  9997  iunctb  9998  pwfseqlem4  10086  pwfseqlem5  10087  pwxpndom2  10089  pwdjundom  10091  gchac  10105  wunex2  10162  tskinf  10193  niex  10305  nnexALT  11642  ltweuz  13332  uzenom  13335  nnenom  13351  axdc4uzlem  13354  seqex  13374  rexpen  15583  cctop  21616  2ndcctbss  22065  2ndcdisj  22066  2ndcdisj2  22067  tx2ndc  22261  met2ndci  23134  snct  30451  bnj852  32195  bnj865  32197  satf  32602  satom  32605  satfv0  32607  satfvsuclem1  32608  satfv1lem  32611  satf00  32623  satf0suclem  32624  satf0suc  32625  sat1el2xp  32628  fmla  32630  fmlasuc0  32633  ex-sategoelel  32670  ex-sategoelelomsuc  32675  ex-sategoelel12  32676  prv1n  32680  trpredex  33078  bj-iomnnom  34543  iunctb2  34686  ctbssinf  34689
 Copyright terms: Public domain W3C validator