Theorem omex 9613

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

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 7875 and Fin = V (the universe of all sets) by fineqv 9228. 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 7886 through peano5 7891 (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 3459	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5292	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9612	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3097	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7891	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 604	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1867	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1961	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∀wral 3079  Vcvv 3455   ⊆ wss 3906  ∅c0 4287  suc csuc 6364  ωcom 7863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734  ax-inf2 9611

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-tr 5220  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-om 7864

This theorem is referenced by:  axinf  9614  inf5  9615  omelon  9616  dfom3  9617  elom3  9618  oancom  9621  isfinite  9622  nnsdom  9624  omenps  9625  omensuc  9626  unbnn3  9629  noinfep  9630  ttrclse  9697  tz9.1  9699  tz9.1c  9700  xpct  10001  fseqdom  10011  fseqen  10012  aleph0  10051  alephprc  10084  alephfplem1  10089  alephfplem4  10092  iunfictbso  10099  unctb  10188  r1om  10227  cfom  10249  itunifval  10401  hsmexlem5  10415  axcc2lem  10421  acncc  10425  axcc4dom  10426  domtriomlem  10427  axdclem2  10505  fnct  10522  infinf  10552  unirnfdomd  10553  alephval2  10558  dominfac  10559  iunctb  10560  pwfseqlem4  10648  pwfseqlem5  10649  pwxpndom2  10651  pwdjundom  10653  gchac  10667  wunex2  10724  tskinf  10755  niex  10867  nnexALT  12236  ltweuz  13999  uzenom  14002  nnenom  14018  axdc4uzlem  14021  seqex  14041  rexpen  16285  cctop  23144  2ndcctbss  23593  2ndcdisj  23594  2ndcdisj2  23595  tx2ndc  23789  met2ndci  24660  n0sex  28491  n0ssold  28528  snct  33038  bnj852  35290  bnj865  35292  r1omfv  35485  satf  35826  satom  35829  satfv0  35831  satfvsuclem1  35832  satfv1lem  35835  satf00  35847  satf0suclem  35848  satf0suc  35849  sat1el2xp  35852  fmla  35854  fmlasuc0  35857  ex-sategoelel  35894  ex-sategoelelomsuc  35899  ex-sategoelel12  35900  prv1n  35904  bj-iomnnom  37884  iunctb2  38030  ctbssinf  38033  succlg  44038  finonex  44163  orbitex  45647