Theorem omex 9622

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

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 7883 and Fin = V (the universe of all sets) by fineqv 9237. 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 7894 through peano5 7899 (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 3462	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5296	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9621	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3100	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7899	. . . 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 2146  ∀wral 3082  Vcvv 3458   ⊆ wss 3908  ∅c0 4289  suc csuc 6369  ωcom 7871

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745  ax-inf2 9620

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-tr 5224  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-om 7872

This theorem is used by:  axinf  9623  inf5  9624  omelon  9625  dfom3  9626  elom3  9627  oancom  9630  isfinite  9631  nnsdom  9633  omenps  9634  omensuc  9635  unbnn3  9638  noinfep  9639  ttrclse  9706  tz9.1  9708  tz9.1c  9709  xpct  10019  fseqdom  10029  fseqen  10030  aleph0  10069  alephprc  10102  alephfplem1  10107  alephfplem4  10110  iunfictbso  10117  unctb  10206  r1om  10245  cfom  10266  itunifval  10418  hsmexlem5  10432  axcc2lem  10438  acncc  10442  axcc4dom  10443  domtriomlem  10444  axdclem2  10522  fnct  10539  infinf  10569  unirnfdomd  10570  alephval2  10575  dominfac  10576  iunctb  10577  pwfseqlem4  10665  pwfseqlem5  10666  pwxpndom2  10668  pwdjundom  10670  gchac  10684  wunex2  10741  tskinf  10772  niex  10884  nnexALT  12253  ltweuz  14017  uzenom  14020  nnenom  14036  axdc4uzlem  14039  seqex  14059  rexpen  16309  cctop  23200  2ndcctbss  23649  2ndcdisj  23650  2ndcdisj2  23651  tx2ndc  23845  met2ndci  24716  n0sex  28547  n0ssold  28584  snct  33094  bnj852  35341  bnj865  35343  r1omfv  35529  satf  35866  satom  35869  satfv0  35871  satfvsuclem1  35872  satfv1lem  35875  satf00  35887  satf0suclem  35888  satf0suc  35889  sat1el2xp  35892  fmla  35894  fmlasuc0  35897  ex-sategoelel  35934  ex-sategoelelomsuc  35939  ex-sategoelel12  35940  prv1n  35944  bj-iomnnom  37944  iunctb2  38090  ctbssinf  38093  succlg  44096  finonex  44221  orbitex  45705