Theorem omex 9401

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

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 7724 and Fin = V (the universe of all sets) by fineqv 9038. 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 7735 through peano5 7740 (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 9400	. 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
3	2	ralimi2 3084	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
4		peano5 7740	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
5	3, 4	sylan2 593	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
6	5	eximi 1837	. 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥)
7		vex 3436	. . . 4 ⊢ 𝑥 ∈ V
8	7	ssex 5245	. . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
9	8	exlimiv 1933	. 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
10	1, 6, 9	mp2b 10	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1782   ∈ wcel 2106  ∀wral 3064  Vcvv 3432   ⊆ wss 3887  ∅c0 4256  suc csuc 6268  ωcom 7712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588  ax-inf2 9399

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-tr 5192  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-om 7713

This theorem is referenced by:  axinf  9402  inf5  9403  omelon  9404  dfom3  9405  elom3  9406  oancom  9409  isfinite  9410  nnsdom  9412  omenps  9413  omensuc  9414  unbnn3  9417  noinfep  9418  ttrclse  9485  tz9.1  9487  tz9.1c  9488  xpct  9772  fseqdom  9782  fseqen  9783  aleph0  9822  alephprc  9855  alephfplem1  9860  alephfplem4  9863  iunfictbso  9870  unctb  9961  r1om  10000  cfom  10020  itunifval  10172  hsmexlem5  10186  axcc2lem  10192  acncc  10196  axcc4dom  10197  domtriomlem  10198  axdclem2  10276  fnct  10293  infinf  10322  unirnfdomd  10323  alephval2  10328  dominfac  10329  iunctb  10330  pwfseqlem4  10418  pwfseqlem5  10419  pwxpndom2  10421  pwdjundom  10423  gchac  10437  wunex2  10494  tskinf  10525  niex  10637  nnexALT  11975  ltweuz  13681  uzenom  13684  nnenom  13700  axdc4uzlem  13703  seqex  13723  rexpen  15937  cctop  22156  2ndcctbss  22606  2ndcdisj  22607  2ndcdisj2  22608  tx2ndc  22802  met2ndci  23678  snct  31048  bnj852  32901  bnj865  32903  satf  33315  satom  33318  satfv0  33320  satfvsuclem1  33321  satfv1lem  33324  satf00  33336  satf0suclem  33337  satf0suc  33338  sat1el2xp  33341  fmla  33343  fmlasuc0  33346  ex-sategoelel  33383  ex-sategoelelomsuc  33388  ex-sategoelel12  33389  prv1n  33393  bj-iomnnom  35430  iunctb2  35574  ctbssinf  35577  finonex  41061