Theorem omex 9533

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

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 7808 and Fin = V (the universe of all sets) by fineqv 9151. 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 7819 through peano5 7823 (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 3440	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5259	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9532	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3064	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7823	. . . 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 2111  ∀wral 3047  Vcvv 3436   ⊆ wss 3902  ∅c0 4283  suc csuc 6308  ωcom 7796

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668  ax-inf2 9531

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-tr 5199  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-om 7797

This theorem is referenced by:  axinf  9534  inf5  9535  omelon  9536  dfom3  9537  elom3  9538  oancom  9541  isfinite  9542  nnsdom  9544  omenps  9545  omensuc  9546  unbnn3  9549  noinfep  9550  ttrclse  9617  tz9.1  9619  tz9.1c  9620  xpct  9907  fseqdom  9917  fseqen  9918  aleph0  9957  alephprc  9990  alephfplem1  9995  alephfplem4  9998  iunfictbso  10005  unctb  10095  r1om  10134  cfom  10155  itunifval  10307  hsmexlem5  10321  axcc2lem  10327  acncc  10331  axcc4dom  10332  domtriomlem  10333  axdclem2  10411  fnct  10428  infinf  10457  unirnfdomd  10458  alephval2  10463  dominfac  10464  iunctb  10465  pwfseqlem4  10553  pwfseqlem5  10554  pwxpndom2  10556  pwdjundom  10558  gchac  10572  wunex2  10629  tskinf  10660  niex  10772  nnexALT  12127  ltweuz  13868  uzenom  13871  nnenom  13887  axdc4uzlem  13890  seqex  13910  rexpen  16137  cctop  22922  2ndcctbss  23371  2ndcdisj  23372  2ndcdisj2  23373  tx2ndc  23567  met2ndci  24438  snct  32693  bnj852  34931  bnj865  34933  r1omfv  35119  satf  35395  satom  35398  satfv0  35400  satfvsuclem1  35401  satfv1lem  35404  satf00  35416  satf0suclem  35417  satf0suc  35418  sat1el2xp  35421  fmla  35423  fmlasuc0  35426  ex-sategoelel  35463  ex-sategoelelomsuc  35468  ex-sategoelel12  35469  prv1n  35473  bj-iomnnom  37299  iunctb2  37443  ctbssinf  37446  succlg  43367  finonex  43493  orbitex  44994