Theorem omex 9600

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

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 7862 and Fin = V (the universe of all sets) by fineqv 9215. 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 7873 through peano5 7878 (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 3461	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5282	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9599	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3097	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7878	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 604	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1860	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1954	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  ∀wral 3079  Vcvv 3457   ⊆ wss 3907  ∅c0 4288  suc csuc 6352  ωcom 7850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722  ax-inf2 9598

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-tr 5213  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-om 7851

This theorem is referenced by:  axinf  9601  inf5  9602  omelon  9603  dfom3  9604  elom3  9605  oancom  9608  isfinite  9609  nnsdom  9611  omenps  9612  omensuc  9613  unbnn3  9616  noinfep  9617  ttrclse  9684  tz9.1  9686  tz9.1c  9687  xpct  9988  fseqdom  9998  fseqen  9999  aleph0  10038  alephprc  10071  alephfplem1  10076  alephfplem4  10079  iunfictbso  10086  unctb  10175  r1om  10214  cfom  10236  itunifval  10388  hsmexlem5  10402  axcc2lem  10408  acncc  10412  axcc4dom  10413  domtriomlem  10414  axdclem2  10492  fnct  10509  infinf  10539  unirnfdomd  10540  alephval2  10545  dominfac  10546  iunctb  10547  pwfseqlem4  10635  pwfseqlem5  10636  pwxpndom2  10638  pwdjundom  10640  gchac  10654  wunex2  10711  tskinf  10742  niex  10854  nnexALT  12226  ltweuz  13988  uzenom  13991  nnenom  14007  axdc4uzlem  14010  seqex  14030  rexpen  16274  cctop  23124  2ndcctbss  23573  2ndcdisj  23574  2ndcdisj2  23575  tx2ndc  23769  met2ndci  24640  n0sex  28468  n0ssold  28505  snct  32969  bnj852  35226  bnj865  35228  r1omfv  35418  satf  35716  satom  35719  satfv0  35721  satfvsuclem1  35722  satfv1lem  35725  satf00  35737  satf0suclem  35738  satf0suc  35739  sat1el2xp  35742  fmla  35744  fmlasuc0  35747  ex-sategoelel  35784  ex-sategoelelomsuc  35789  ex-sategoelel12  35790  prv1n  35794  bj-iomnnom  37763  iunctb2  37909  ctbssinf  37912  succlg  43917  finonex  44042  orbitex  45529