Theorem omex 9626

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

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 7878 and Fin = V (the universe of all sets) by fineqv 9241. 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 7889 through peano5 7894 (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 3457	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5289	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9625	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3096	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7894	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 605	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1870	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1964	1 ⊢ ω ∈ V

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3078  Vcvv 3453   ⊆ wss 3902  ∅c0 4282  suc csuc 6363  ωcom 7866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740  ax-inf2 9624

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-tr 5217  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-om 7867

This theorem is used by:  axinf  9627  inf5  9628  omelon  9629  dfom3  9630  elom3  9631  oancom  9634  isfinite  9635  nnsdom  9637  omenps  9638  omensuc  9639  unbnn3  9642  noinfep  9643  ttrclse  9710  tz9.1  9712  tz9.1c  9713  xpct  10023  fseqdom  10033  fseqen  10034  aleph0  10073  alephprc  10106  alephfplem1  10111  alephfplem4  10114  iunfictbso  10121  unctb  10210  r1om  10249  cfom  10270  itunifval  10422  hsmexlem5  10436  axcc2lem  10442  acncc  10446  axcc4dom  10447  domtriomlem  10448  axdclem2  10526  fnct  10548  fnctOLD  10549  infinf  10579  unirnfdomd  10580  alephval2  10585  dominfac  10586  iunctb  10587  pwfseqlem4  10675  pwfseqlem5  10676  pwxpndom2  10678  pwdjundom  10680  gchac  10694  wunex2  10751  tskinf  10782  niex  10894  nnexALT  12263  ltweuz  14029  uzenom  14032  nnenom  14048  axdc4uzlem  14051  seqex  14071  rexpen  16322  cctop  23237  2ndcctbss  23687  2ndcdisj  23688  2ndcdisj2  23689  tx2ndc  23883  met2ndci  24754  n0sex  28590  n0ssold  28627  snct  33192  bnj852  35438  bnj865  35440  r1omfv  35626  satf  35940  satom  35943  satfv0  35945  satfvsuclem1  35946  satfv1lem  35949  satf00  35961  satf0suclem  35962  satf0suc  35963  sat1el2xp  35966  fmla  35968  fmlasuc0  35971  ex-sategoelel  36008  ex-sategoelelomsuc  36013  ex-sategoelel12  36014  prv1n  36018  bj-iomnnom  38019  iunctb2  38165  ctbssinf  38168  succlg  44177  finonex  44302  orbitex  45786