Theorem omex 9552

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

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 7820 and Fin = V (the universe of all sets) by fineqv 9167. 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 7831 through peano5 7835 (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 3444	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5266	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9551	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3068	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7835	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 593	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1838	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1932	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3051  Vcvv 3440   ⊆ wss 3901  ∅c0 4285  suc csuc 6319  ωcom 7808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-inf2 9550

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-tr 5206  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-om 7809

This theorem is referenced by:  axinf  9553  inf5  9554  omelon  9555  dfom3  9556  elom3  9557  oancom  9560  isfinite  9561  nnsdom  9563  omenps  9564  omensuc  9565  unbnn3  9568  noinfep  9569  ttrclse  9636  tz9.1  9638  tz9.1c  9639  xpct  9926  fseqdom  9936  fseqen  9937  aleph0  9976  alephprc  10009  alephfplem1  10014  alephfplem4  10017  iunfictbso  10024  unctb  10114  r1om  10153  cfom  10174  itunifval  10326  hsmexlem5  10340  axcc2lem  10346  acncc  10350  axcc4dom  10351  domtriomlem  10352  axdclem2  10430  fnct  10447  infinf  10477  unirnfdomd  10478  alephval2  10483  dominfac  10484  iunctb  10485  pwfseqlem4  10573  pwfseqlem5  10574  pwxpndom2  10576  pwdjundom  10578  gchac  10592  wunex2  10649  tskinf  10680  niex  10792  nnexALT  12147  ltweuz  13884  uzenom  13887  nnenom  13903  axdc4uzlem  13906  seqex  13926  rexpen  16153  cctop  22950  2ndcctbss  23399  2ndcdisj  23400  2ndcdisj2  23401  tx2ndc  23595  met2ndci  24466  n0sex  28313  n0ssold  28350  snct  32791  bnj852  35077  bnj865  35079  r1omfv  35266  satf  35547  satom  35550  satfv0  35552  satfvsuclem1  35553  satfv1lem  35556  satf00  35568  satf0suclem  35569  satf0suc  35570  sat1el2xp  35573  fmla  35575  fmlasuc0  35578  ex-sategoelel  35615  ex-sategoelelomsuc  35620  ex-sategoelel12  35621  prv1n  35625  bj-iomnnom  37464  iunctb2  37608  ctbssinf  37611  succlg  43570  finonex  43695  orbitex  45196