Theorem omex 9628

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

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 9242. 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 3455	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5282	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9627	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3095	. . . 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 3077  Vcvv 3451   ⊆ wss 3899  ∅c0 4279  suc csuc 6357  ω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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740  ax-inf2 9626

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-om 7867

This theorem is used by:  axinf  9629  inf5  9630  omelon  9631  dfom3  9632  elom3  9633  oancom  9636  isfinite  9637  nnsdom  9639  omenps  9640  omensuc  9641  unbnn3  9644  noinfep  9645  ttrclse  9712  tz9.1  9714  tz9.1c  9715  dfhf2  9887  xpct  10076  fseqdom  10086  fseqen  10087  aleph0  10126  alephprc  10159  alephfplem1  10164  alephfplem4  10167  iunfictbso  10174  unctb  10263  cfom  10323  itunifval  10475  hsmexlem5  10489  axcc2lem  10495  acncc  10499  axcc4dom  10500  domtriomlem  10501  axdclem2  10579  fnct  10601  fnctOLD  10602  infinf  10632  unirnfdomd  10633  alephval2  10638  dominfac  10639  iunctb  10640  pwfseqlem4  10728  pwfseqlem5  10729  pwxpndom2  10731  pwdjundom  10733  gchac  10747  wunex2  10804  tskinf  10835  niex  10947  nnexALT  12318  ltweuz  14084  uzenom  14087  nnenom  14103  axdc4uzlem  14106  seqex  14126  rexpen  16376  cctop  23304  2ndcctbss  23754  2ndcdisj  23755  2ndcdisj2  23756  tx2ndc  23950  met2ndci  24821  n0sex  28685  n0ssold  28722  snct  33287  bnj852  35534  bnj865  35536  satf  36087  satom  36090  satfv0  36092  satfvsuclem1  36093  satfv1lem  36096  satf00  36108  satf0suclem  36109  satf0suc  36110  sat1el2xp  36113  fmla  36115  fmlasuc0  36118  ex-sategoelel  36155  ex-sategoelelomsuc  36160  ex-sategoelel12  36161  prv1n  36165  bj-iomnnom  38148  iunctb2  38294  ctbssinf  38297  succlg  44288  finonex  44413  orbitex  45897