Theorem omex 9603

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

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 7857 and Fin = V (the universe of all sets) by fineqv 9217. 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 7868 through peano5 7872 (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 3454	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5279	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9602	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3062	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7872	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 593	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1837	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1931	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3045  Vcvv 3450   ⊆ wss 3917  ∅c0 4299  suc csuc 6337  ωcom 7845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-inf2 9601

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-om 7846

This theorem is referenced by:  axinf  9604  inf5  9605  omelon  9606  dfom3  9607  elom3  9608  oancom  9611  isfinite  9612  nnsdom  9614  omenps  9615  omensuc  9616  unbnn3  9619  noinfep  9620  ttrclse  9687  tz9.1  9689  tz9.1c  9690  xpct  9976  fseqdom  9986  fseqen  9987  aleph0  10026  alephprc  10059  alephfplem1  10064  alephfplem4  10067  iunfictbso  10074  unctb  10164  r1om  10203  cfom  10224  itunifval  10376  hsmexlem5  10390  axcc2lem  10396  acncc  10400  axcc4dom  10401  domtriomlem  10402  axdclem2  10480  fnct  10497  infinf  10526  unirnfdomd  10527  alephval2  10532  dominfac  10533  iunctb  10534  pwfseqlem4  10622  pwfseqlem5  10623  pwxpndom2  10625  pwdjundom  10627  gchac  10641  wunex2  10698  tskinf  10729  niex  10841  nnexALT  12195  ltweuz  13933  uzenom  13936  nnenom  13952  axdc4uzlem  13955  seqex  13975  rexpen  16203  cctop  22900  2ndcctbss  23349  2ndcdisj  23350  2ndcdisj2  23351  tx2ndc  23545  met2ndci  24417  snct  32644  bnj852  34918  bnj865  34920  satf  35347  satom  35350  satfv0  35352  satfvsuclem1  35353  satfv1lem  35356  satf00  35368  satf0suclem  35369  satf0suc  35370  sat1el2xp  35373  fmla  35375  fmlasuc0  35378  ex-sategoelel  35415  ex-sategoelelomsuc  35420  ex-sategoelel12  35421  prv1n  35425  bj-iomnnom  37254  iunctb2  37398  ctbssinf  37401  succlg  43324  finonex  43450  orbitex  44952