Theorem omex 9172

Description: The existence of omega (the class of natural numbers). Axiom 7 of [TakeutiZaring] p. 43. This theorem is proved assuming the Axiom of Infinity and in fact is equivalent to it, as shown by the reverse derivation inf0 9150.

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 7604 and Fin = V (the universe of all sets) by fineqv 8805. 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 7614 through peano5 7618 (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		zfinf2 9171	. 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
3	2	ralimi2 3072	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
4		peano5 7618	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
5	3, 4	sylan2 596	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
6	5	eximi 1841	. 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥)
7		vex 3401	. . . 4 ⊢ 𝑥 ∈ V
8	7	ssex 5186	. . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
9	8	exlimiv 1936	. 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
10	1, 6, 9	mp2b 10	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1786   ∈ wcel 2113  ∀wral 3053  Vcvv 3397   ⊆ wss 3841  ∅c0 4209  suc csuc 6168  ωcom 7593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293  ax-un 7473  ax-inf2 9170

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3399  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-br 5028  df-opab 5090  df-tr 5134  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-om 7594

This theorem is referenced by:  axinf  9173  inf5  9174  omelon  9175  dfom3  9176  elom3  9177  oancom  9180  isfinite  9181  nnsdom  9183  omenps  9184  omensuc  9185  unbnn3  9188  noinfep  9189  tz9.1  9237  tz9.1c  9238  xpct  9509  fseqdom  9519  fseqen  9520  aleph0  9559  alephprc  9592  alephfplem1  9597  alephfplem4  9600  iunfictbso  9607  unctb  9698  r1om  9737  cfom  9757  itunifval  9909  hsmexlem5  9923  axcc2lem  9929  acncc  9933  axcc4dom  9934  domtriomlem  9935  axdclem2  10013  fnct  10030  infinf  10059  unirnfdomd  10060  alephval2  10065  dominfac  10066  iunctb  10067  pwfseqlem4  10155  pwfseqlem5  10156  pwxpndom2  10158  pwdjundom  10160  gchac  10174  wunex2  10231  tskinf  10262  niex  10374  nnexALT  11711  ltweuz  13413  uzenom  13416  nnenom  13432  axdc4uzlem  13435  seqex  13455  rexpen  15666  cctop  21750  2ndcctbss  22199  2ndcdisj  22200  2ndcdisj2  22201  tx2ndc  22395  met2ndci  23268  snct  30615  bnj852  32464  bnj865  32466  satf  32878  satom  32881  satfv0  32883  satfvsuclem1  32884  satfv1lem  32887  satf00  32899  satf0suclem  32900  satf0suc  32901  sat1el2xp  32904  fmla  32906  fmlasuc0  32909  ex-sategoelel  32946  ex-sategoelelomsuc  32951  ex-sategoelel12  32952  prv1n  32956  trpredex  33371  bj-iomnnom  35040  iunctb2  35186  ctbssinf  35189