Theorem omex 9712

Description: The existence of omega (the class of natural numbers). Axiom 7 of [TakeutiZaring] p. 43. Remark 1.21 of [Schloeder] p. 3. This theorem is proved assuming the Axiom of Infinity and in fact is equivalent to it, as shown by the reverse derivation inf0 9690.

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 7915 and Fin = V (the universe of all sets) by fineqv 9326. 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 7927 through peano5 7932 (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.

Step	Hyp	Ref	Expression
1		zfinf2 9711	. 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
3	2	ralimi2 3084	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
4		peano5 7932	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
5	3, 4	sylan2 592	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
6	5	eximi 1833	. 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥)
7		vex 3492	. . . 4 ⊢ 𝑥 ∈ V
8	7	ssex 5339	. . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
9	8	exlimiv 1929	. 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
10	1, 6, 9	mp2b 10	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1777   ∈ wcel 2108  ∀wral 3067  Vcvv 3488   ⊆ wss 3976  ∅c0 4352  suc csuc 6397  ωcom 7903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-inf2 9710

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-om 7904

This theorem is referenced by:  axinf  9713  inf5  9714  omelon  9715  dfom3  9716  elom3  9717  oancom  9720  isfinite  9721  nnsdom  9723  omenps  9724  omensuc  9725  unbnn3  9728  noinfep  9729  ttrclse  9796  tz9.1  9798  tz9.1c  9799  xpct  10085  fseqdom  10095  fseqen  10096  aleph0  10135  alephprc  10168  alephfplem1  10173  alephfplem4  10176  iunfictbso  10183  unctb  10273  r1om  10312  cfom  10333  itunifval  10485  hsmexlem5  10499  axcc2lem  10505  acncc  10509  axcc4dom  10510  domtriomlem  10511  axdclem2  10589  fnct  10606  infinf  10635  unirnfdomd  10636  alephval2  10641  dominfac  10642  iunctb  10643  pwfseqlem4  10731  pwfseqlem5  10732  pwxpndom2  10734  pwdjundom  10736  gchac  10750  wunex2  10807  tskinf  10838  niex  10950  nnexALT  12295  ltweuz  14012  uzenom  14015  nnenom  14031  axdc4uzlem  14034  seqex  14054  rexpen  16276  cctop  23034  2ndcctbss  23484  2ndcdisj  23485  2ndcdisj2  23486  tx2ndc  23680  met2ndci  24556  snct  32727  bnj852  34897  bnj865  34899  satf  35321  satom  35324  satfv0  35326  satfvsuclem1  35327  satfv1lem  35330  satf00  35342  satf0suclem  35343  satf0suc  35344  sat1el2xp  35347  fmla  35349  fmlasuc0  35352  ex-sategoelel  35389  ex-sategoelelomsuc  35394  ex-sategoelel12  35395  prv1n  35399  bj-iomnnom  37225  iunctb2  37369  ctbssinf  37372  succlg  43290  finonex  43416