Theorem omex 9542

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 9520.

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 7816 and Fin = V (the universe of all sets) by fineqv 9160. 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 7827 through peano5 7831 (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		vex 3441	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5263	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9541	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3065	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7831	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 593	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1838	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1932	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3048  Vcvv 3437   ⊆ wss 3898  ∅c0 4282  suc csuc 6315  ωcom 7804

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7676  ax-inf2 9540

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-om 7805

This theorem is referenced by:  axinf  9543  inf5  9544  omelon  9545  dfom3  9546  elom3  9547  oancom  9550  isfinite  9551  nnsdom  9553  omenps  9554  omensuc  9555  unbnn3  9558  noinfep  9559  ttrclse  9626  tz9.1  9628  tz9.1c  9629  xpct  9916  fseqdom  9926  fseqen  9927  aleph0  9966  alephprc  9999  alephfplem1  10004  alephfplem4  10007  iunfictbso  10014  unctb  10104  r1om  10143  cfom  10164  itunifval  10316  hsmexlem5  10330  axcc2lem  10336  acncc  10340  axcc4dom  10341  domtriomlem  10342  axdclem2  10420  fnct  10437  infinf  10466  unirnfdomd  10467  alephval2  10472  dominfac  10473  iunctb  10474  pwfseqlem4  10562  pwfseqlem5  10563  pwxpndom2  10565  pwdjundom  10567  gchac  10581  wunex2  10638  tskinf  10669  niex  10781  nnexALT  12136  ltweuz  13872  uzenom  13875  nnenom  13891  axdc4uzlem  13894  seqex  13914  rexpen  16141  cctop  22924  2ndcctbss  23373  2ndcdisj  23374  2ndcdisj2  23375  tx2ndc  23569  met2ndci  24440  snct  32701  bnj852  34956  bnj865  34958  r1omfv  35144  satf  35420  satom  35423  satfv0  35425  satfvsuclem1  35426  satfv1lem  35429  satf00  35441  satf0suclem  35442  satf0suc  35443  sat1el2xp  35446  fmla  35448  fmlasuc0  35451  ex-sategoelel  35488  ex-sategoelelomsuc  35493  ex-sategoelel12  35494  prv1n  35498  bj-iomnnom  37326  iunctb2  37470  ctbssinf  37473  succlg  43448  finonex  43574  orbitex  45075