Theorem omex 9106

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

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 7591 and Fin = V (the universe of all sets) by fineqv 8733. 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 7601 through peano5 7605 (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 9105	. 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
3	2	ralimi2 3157	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
4		peano5 7605	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
5	3, 4	sylan2 594	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
6	5	eximi 1835	. 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥)
7		vex 3497	. . . 4 ⊢ 𝑥 ∈ V
8	7	ssex 5225	. . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
9	8	exlimiv 1931	. 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
10	1, 6, 9	mp2b 10	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  ∀wral 3138  Vcvv 3494   ⊆ wss 3936  ∅c0 4291  suc csuc 6193  ωcom 7580

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330  ax-un 7461  ax-inf2 9104

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-tr 5173  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-om 7581

This theorem is referenced by:  axinf  9107  inf5  9108  omelon  9109  dfom3  9110  elom3  9111  oancom  9114  isfinite  9115  nnsdom  9117  omenps  9118  omensuc  9119  unbnn3  9122  noinfep  9123  tz9.1  9171  tz9.1c  9172  xpct  9442  fseqdom  9452  fseqen  9453  aleph0  9492  alephprc  9525  alephfplem1  9530  alephfplem4  9533  iunfictbso  9540  unctb  9627  r1om  9666  cfom  9686  itunifval  9838  hsmexlem5  9852  axcc2lem  9858  acncc  9862  axcc4dom  9863  domtriomlem  9864  axdclem2  9942  fnct  9959  infinf  9988  unirnfdomd  9989  alephval2  9994  dominfac  9995  iunctb  9996  pwfseqlem4  10084  pwfseqlem5  10085  pwxpndom2  10087  pwdjundom  10089  gchac  10103  wunex2  10160  tskinf  10191  niex  10303  nnexALT  11640  ltweuz  13330  uzenom  13333  nnenom  13349  axdc4uzlem  13352  seqex  13372  rexpen  15581  cctop  21614  2ndcctbss  22063  2ndcdisj  22064  2ndcdisj2  22065  tx2ndc  22259  met2ndci  23132  snct  30449  bnj852  32193  bnj865  32195  satf  32600  satom  32603  satfv0  32605  satfvsuclem1  32606  satfv1lem  32609  satf00  32621  satf0suclem  32622  satf0suc  32623  sat1el2xp  32626  fmla  32628  fmlasuc0  32631  ex-sategoelel  32668  ex-sategoelelomsuc  32673  ex-sategoelel12  32674  prv1n  32678  trpredex  33076  bj-iomnnom  34544  iunctb2  34687  ctbssinf  34690