Theorem omex 4614

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

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 (the proper class of ordinals) by omon 3140 and onprc 2986. 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 3146 through peano5 3150 (which many textbooks prove more easily assuming Infinity).

Assertion

Ref	Expression
omex	⊢ ω ∈ V

Proof of Theorem omex

Step	Hyp	Ref	Expression
1		zfinf 4613	. . 3 ⊢ ∃x(∅ ∈ x ⋀ ∀y ∈ x suc y ∈ x)
2		peano5 3150	. . . . 5 ⊢ ((∅ ∈ x ⋀ ∀y ∈ ω (y ∈ x → suc y ∈ x)) → ω ⊆ x)
3		ax-1 4	. . . . . 6 ⊢ ((y ∈ x → suc y ∈ x) → (y ∈ ω → (y ∈ x → suc y ∈ x)))
4	3	r19.20i2 1702	. . . . 5 ⊢ (∀y ∈ x suc y ∈ x → ∀y ∈ ω (y ∈ x → suc y ∈ x))
5	2, 4	sylan2 451	. . . 4 ⊢ ((∅ ∈ x ⋀ ∀y ∈ x suc y ∈ x) → ω ⊆ x)
6	5	19.22i 1039	. . 3 ⊢ (∃x(∅ ∈ x ⋀ ∀y ∈ x suc y ∈ x) → ∃xω ⊆ x)
7	1, 6	ax-mp 7	. 2 ⊢ ∃xω ⊆ x
8		visset 1811	. . . 4 ⊢ x ∈ V
9	8	ssex 2716	. . 3 ⊢ (ω ⊆ x → ω ∈ V)
10	9	19.23aiv 1295	. 2 ⊢ (∃xω ⊆ x → ω ∈ V)
11	7, 10	ax-mp 7	1 ⊢ ω ∈ V

Syntax hints:   → wi 3   ⋀ wa 223   ∈ wcel 957  ∃wex 979  ∀wral 1644  Vcvv 1809   ⊆ wss 2045  ∅c0 2278  suc csuc 2947  ωcom 3128

This theorem is referenced by:  inf5 4615  omelon 4616  dfom3 4617  elom3 4618  oancom 4620  isfinite 4621  nnsdom 4622  omenps 4623  omensuc 4624  unbnnt 4626  noinfep 4627  tz9.1 4633  sucdom 4829  aleph0 4850  alephprc 4880  alephfplem4 4886  alephval2 4889  dominf 4891  cfom 4903  cdainf 4924  niex 4996  nnenom 7476  xpomen 7478  unben 7484  aleph1re 7530  infxpidmlem10 7540  infdif 7547  iunctb 7554  aleph1irr 7557

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2700  ax-nul 2707  ax-pow 2739  ax-pr 2776  ax-un 2863  ax-inf2 4612

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-ral 1648  df-rex 1649  df-v 1810  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-nul 2279  df-if 2360  df-pw 2400  df-sn 2410  df-pr 2411  df-tp 2413  df-op 2414  df-uni 2501  df-br 2617  df-opab 2664  df-tr 2678  df-eprel 2829  df-po 2837  df-so 2847  df-fr 2914  df-we 2931  df-ord 2948  df-on 2949  df-lim 2950  df-suc 2951  df-om 3129

Copyright terms: Public domain