Definition df-inn 9008

Description: Definition of the set of positive integers. For naming consistency with the Metamath Proof Explorer usages should refer to dfnn2 9009 instead. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.) (New usage is discouraged.)

Assertion

Ref	Expression
df-inn	⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-inn

Step	Hyp	Ref	Expression
1		cn 9007	. 2 class ℕ
2		c1 7897	. . . . . 6 class 1
3		vx	. . . . . . 7 setvar 𝑥
4	3	cv 1363	. . . . . 6 class 𝑥
5	2, 4	wcel 2167	. . . . 5 wff 1 ∈ 𝑥
6		vy	. . . . . . . . 9 setvar 𝑦
7	6	cv 1363	. . . . . . . 8 class 𝑦
8		caddc 7899	. . . . . . . 8 class +
9	7, 2, 8	co 5925	. . . . . . 7 class (𝑦 + 1)
10	9, 4	wcel 2167	. . . . . 6 wff (𝑦 + 1) ∈ 𝑥
11	10, 6, 4	wral 2475	. . . . 5 wff ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥
12	5, 11	wa 104	. . . 4 wff (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)
13	12, 3	cab 2182	. . 3 class {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
14	13	cint 3875	. 2 class ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
15	1, 14	wceq 1364	1 wff ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}

This definition is referenced by:  dfnn2  9009