Theorem dfom3 9537

Description: The class of natural numbers ω can be defined as the intersection of all inductive sets (which is the smallest inductive set, since inductive sets are closed under intersection), which is valid provided we assume the Axiom of Infinity. Definition 6.3 of [Eisenberg] p. 82. Definition 1.20 of [Schloeder] p. 3. (Contributed by NM, 6-Aug-1994.)

Assertion

Ref	Expression
dfom3	⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}

Distinct variable group:   𝑥,𝑦

Proof of Theorem dfom3

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 5243	. . . . 5 ⊢ ∅ ∈ V
2	1	elintab 4907	. . . 4 ⊢ (∅ ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∅ ∈ 𝑥))
3		simpl 482	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∅ ∈ 𝑥)
4	2, 3	mpgbir 1800	. . 3 ⊢ ∅ ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
5		suceq 6374	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧)
6	5	eleq1d 2816	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (suc 𝑦 ∈ 𝑥 ↔ suc 𝑧 ∈ 𝑥))
7	6	rspccv 3569	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → (𝑧 ∈ 𝑥 → suc 𝑧 ∈ 𝑥))
8	7	adantl 481	. . . . . . 7 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → (𝑧 ∈ 𝑥 → suc 𝑧 ∈ 𝑥))
9	8	a2i 14	. . . . . 6 ⊢ (((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → suc 𝑧 ∈ 𝑥))
10	9	alimi 1812	. . . . 5 ⊢ (∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → suc 𝑧 ∈ 𝑥))
11		vex 3440	. . . . . 6 ⊢ 𝑧 ∈ V
12	11	elintab 4907	. . . . 5 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
13	11	sucex 7739	. . . . . 6 ⊢ suc 𝑧 ∈ V
14	13	elintab 4907	. . . . 5 ⊢ (suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → suc 𝑧 ∈ 𝑥))
15	10, 12, 14	3imtr4i 292	. . . 4 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})
16	15	rgenw 3051	. . 3 ⊢ ∀𝑧 ∈ ω (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})
17		peano5 7823	. . 3 ⊢ ((∅ ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ∧ ∀𝑧 ∈ ω (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})) → ω ⊆ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})
18	4, 16, 17	mp2an 692	. 2 ⊢ ω ⊆ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
19		peano1 7819	. . . 4 ⊢ ∅ ∈ ω
20		peano2 7820	. . . . 5 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
21	20	rgen 3049	. . . 4 ⊢ ∀𝑦 ∈ ω suc 𝑦 ∈ ω
22		omex 9533	. . . . . 6 ⊢ ω ∈ V
23		eleq2 2820	. . . . . . . 8 ⊢ (𝑥 = ω → (∅ ∈ 𝑥 ↔ ∅ ∈ ω))
24		eleq2 2820	. . . . . . . . 9 ⊢ (𝑥 = ω → (suc 𝑦 ∈ 𝑥 ↔ suc 𝑦 ∈ ω))
25	24	raleqbi1dv 3304	. . . . . . . 8 ⊢ (𝑥 = ω → (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ↔ ∀𝑦 ∈ ω suc 𝑦 ∈ ω))
26	23, 25	anbi12d 632	. . . . . . 7 ⊢ (𝑥 = ω → ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) ↔ (∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω)))
27		eleq2 2820	. . . . . . 7 ⊢ (𝑥 = ω → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ ω))
28	26, 27	imbi12d 344	. . . . . 6 ⊢ (𝑥 = ω → (((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω) → 𝑧 ∈ ω)))
29	22, 28	spcv 3555	. . . . 5 ⊢ (∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → ((∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω) → 𝑧 ∈ ω))
30	12, 29	sylbi 217	. . . 4 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → ((∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω) → 𝑧 ∈ ω))
31	19, 21, 30	mp2ani 698	. . 3 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → 𝑧 ∈ ω)
32	31	ssriv 3933	. 2 ⊢ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ⊆ ω
33	18, 32	eqssi 3946	1 ⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1539   = wceq 1541   ∈ wcel 2111  {cab 2709  ∀wral 3047   ⊆ wss 3897  ∅c0 4280  ∩ cint 4895  suc csuc 6308  ωcom 7796

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668  ax-inf2 9531

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-int 4896  df-br 5090  df-opab 5152  df-tr 5197  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-om 7797

This theorem is referenced by: (None)