Theorem dfom3 9562

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 4902	. . . 4 ⊢ (∅ ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∅ ∈ 𝑥))
3		simpl 482	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∅ ∈ 𝑥)
4	2, 3	mpgbir 1801	. . 3 ⊢ ∅ ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
5		suceq 6386	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧)
6	5	eleq1d 2822	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (suc 𝑦 ∈ 𝑥 ↔ suc 𝑧 ∈ 𝑥))
7	6	rspccv 3562	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → (𝑧 ∈ 𝑥 → suc 𝑧 ∈ 𝑥))
8	7	adantl 481	. . . . . . 7 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → (𝑧 ∈ 𝑥 → suc 𝑧 ∈ 𝑥))
9	8	a2i 14	. . . . . 6 ⊢ (((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → suc 𝑧 ∈ 𝑥))
10	9	alimi 1813	. . . . 5 ⊢ (∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → suc 𝑧 ∈ 𝑥))
11		vex 3434	. . . . . 6 ⊢ 𝑧 ∈ V
12	11	elintab 4902	. . . . 5 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
13	11	sucex 7754	. . . . . 6 ⊢ suc 𝑧 ∈ V
14	13	elintab 4902	. . . . 5 ⊢ (suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → suc 𝑧 ∈ 𝑥))
15	10, 12, 14	3imtr4i 292	. . . 4 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})
16	15	rgenw 3056	. . 3 ⊢ ∀𝑧 ∈ ω (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})
17		peano5 7838	. . 3 ⊢ ((∅ ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ∧ ∀𝑧 ∈ ω (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})) → ω ⊆ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})
18	4, 16, 17	mp2an 693	. 2 ⊢ ω ⊆ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
19		peano1 7834	. . . 4 ⊢ ∅ ∈ ω
20		peano2 7835	. . . . 5 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
21	20	rgen 3054	. . . 4 ⊢ ∀𝑦 ∈ ω suc 𝑦 ∈ ω
22		omex 9558	. . . . . 6 ⊢ ω ∈ V
23		eleq2 2826	. . . . . . . 8 ⊢ (𝑥 = ω → (∅ ∈ 𝑥 ↔ ∅ ∈ ω))
24		eleq2 2826	. . . . . . . . 9 ⊢ (𝑥 = ω → (suc 𝑦 ∈ 𝑥 ↔ suc 𝑦 ∈ ω))
25	24	raleqbi1dv 3306	. . . . . . . 8 ⊢ (𝑥 = ω → (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ↔ ∀𝑦 ∈ ω suc 𝑦 ∈ ω))
26	23, 25	anbi12d 633	. . . . . . 7 ⊢ (𝑥 = ω → ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) ↔ (∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω)))
27		eleq2 2826	. . . . . . 7 ⊢ (𝑥 = ω → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ ω))
28	26, 27	imbi12d 344	. . . . . 6 ⊢ (𝑥 = ω → (((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω) → 𝑧 ∈ ω)))
29	22, 28	spcv 3548	. . . . 5 ⊢ (∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → ((∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω) → 𝑧 ∈ ω))
30	12, 29	sylbi 217	. . . 4 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → ((∅ ∈ ω ∧ ∀𝑦 ∈ ω suc 𝑦 ∈ ω) → 𝑧 ∈ ω))
31	19, 21, 30	mp2ani 699	. . 3 ⊢ (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → 𝑧 ∈ ω)
32	31	ssriv 3926	. 2 ⊢ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ⊆ ω
33	18, 32	eqssi 3939	1 ⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540   = wceq 1542   ∈ wcel 2114  {cab 2715  ∀wral 3052   ⊆ wss 3890  ∅c0 4274  ∩ cint 4890  suc csuc 6320  ωcom 7811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-inf2 9556

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-om 7812

This theorem is referenced by: (None)