Theorem omex 9596

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

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 7854 and Fin = V (the universe of all sets) by fineqv 9210. 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 7865 through peano5 7869 (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 3451	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5276	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9595	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3061	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7869	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 593	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1837	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1931	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044  Vcvv 3447   ⊆ wss 3914  ∅c0 4296  suc csuc 6334  ωcom 7842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-inf2 9594

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-om 7843

This theorem is referenced by:  axinf  9597  inf5  9598  omelon  9599  dfom3  9600  elom3  9601  oancom  9604  isfinite  9605  nnsdom  9607  omenps  9608  omensuc  9609  unbnn3  9612  noinfep  9613  ttrclse  9680  tz9.1  9682  tz9.1c  9683  xpct  9969  fseqdom  9979  fseqen  9980  aleph0  10019  alephprc  10052  alephfplem1  10057  alephfplem4  10060  iunfictbso  10067  unctb  10157  r1om  10196  cfom  10217  itunifval  10369  hsmexlem5  10383  axcc2lem  10389  acncc  10393  axcc4dom  10394  domtriomlem  10395  axdclem2  10473  fnct  10490  infinf  10519  unirnfdomd  10520  alephval2  10525  dominfac  10526  iunctb  10527  pwfseqlem4  10615  pwfseqlem5  10616  pwxpndom2  10618  pwdjundom  10620  gchac  10634  wunex2  10691  tskinf  10722  niex  10834  nnexALT  12188  ltweuz  13926  uzenom  13929  nnenom  13945  axdc4uzlem  13948  seqex  13968  rexpen  16196  cctop  22893  2ndcctbss  23342  2ndcdisj  23343  2ndcdisj2  23344  tx2ndc  23538  met2ndci  24410  snct  32637  bnj852  34911  bnj865  34913  satf  35340  satom  35343  satfv0  35345  satfvsuclem1  35346  satfv1lem  35349  satf00  35361  satf0suclem  35362  satf0suc  35363  sat1el2xp  35366  fmla  35368  fmlasuc0  35371  ex-sategoelel  35408  ex-sategoelelomsuc  35413  ex-sategoelel12  35414  prv1n  35418  bj-iomnnom  37247  iunctb2  37391  ctbssinf  37394  succlg  43317  finonex  43443  orbitex  44945