Theorem dfom3 9554

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 5250	. . . . 5 ⊢ ∅ ∈ V
2	1	elintab 4912	. . . 4 ⊢ (∅ ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∅ ∈ 𝑥))
3		simpl 482	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∅ ∈ 𝑥)
4	2, 3	mpgbir 1800	. . 3 ⊢ ∅ ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
5		suceq 6383	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧)
6	5	eleq1d 2819	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (suc 𝑦 ∈ 𝑥 ↔ suc 𝑧 ∈ 𝑥))
7	6	rspccv 3571	. . . . . . . 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 3442	. . . . . 6 ⊢ 𝑧 ∈ V
12	11	elintab 4912	. . . . 5 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
13	11	sucex 7749	. . . . . 6 ⊢ suc 𝑧 ∈ V
14	13	elintab 4912	. . . . 5 ⊢ (suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → suc 𝑧 ∈ 𝑥))
15	10, 12, 14	3imtr4i 292	. . . 4 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})
16	15	rgenw 3053	. . 3 ⊢ ∀𝑧 ∈ ω (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})
17		peano5 7833	. . 3 ⊢ ((∅ ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ∧ ∀𝑧 ∈ ω (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})) → ω ⊆ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})
18	4, 16, 17	mp2an 692	. 2 ⊢ ω ⊆ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
19		peano1 7829	. . . 4 ⊢ ∅ ∈ ω
20		peano2 7830	. . . . 5 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
21	20	rgen 3051	. . . 4 ⊢ ∀𝑦 ∈ ω suc 𝑦 ∈ ω
22		omex 9550	. . . . . 6 ⊢ ω ∈ V
23		eleq2 2823	. . . . . . . 8 ⊢ (𝑥 = ω → (∅ ∈ 𝑥 ↔ ∅ ∈ ω))
24		eleq2 2823	. . . . . . . . 9 ⊢ (𝑥 = ω → (suc 𝑦 ∈ 𝑥 ↔ suc 𝑦 ∈ ω))
25	24	raleqbi1dv 3306	. . . . . . . 8 ⊢ (𝑥 = ω → (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ↔ ∀𝑦 ∈ ω suc 𝑦 ∈ ω))
26	23, 25	anbi12d 632	. . . . . . 7 ⊢ (𝑥 = ω → ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) ↔ (∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω)))
27		eleq2 2823	. . . . . . 7 ⊢ (𝑥 = ω → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ ω))
28	26, 27	imbi12d 344	. . . . . 6 ⊢ (𝑥 = ω → (((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω) → 𝑧 ∈ ω)))
29	22, 28	spcv 3557	. . . . 5 ⊢ (∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → ((∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω) → 𝑧 ∈ ω))
30	12, 29	sylbi 217	. . . 4 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → ((∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω) → 𝑧 ∈ ω))
31	19, 21, 30	mp2ani 698	. . 3 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → 𝑧 ∈ ω)
32	31	ssriv 3935	. 2 ⊢ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ⊆ ω
33	18, 32	eqssi 3948	1 ⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1539   = wceq 1541   ∈ wcel 2113  {cab 2712  ∀wral 3049   ⊆ wss 3899  ∅c0 4283  ∩ cint 4900  suc csuc 6317  ωcom 7806

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678  ax-inf2 9548

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 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-int 4901  df-br 5097  df-opab 5159  df-tr 5204  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-om 7807

This theorem is referenced by: (None)