ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-inn GIF version

Definition df-inn 8361
Description: Definition of the set of positive integers. For naming consistency with the Metamath Proof Explorer usages should refer to dfnn2 8362 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
StepHypRef Expression
1 cn 8360 . 2 class
2 c1 7298 . . . . . 6 class 1
3 vx . . . . . . 7 setvar 𝑥
43cv 1286 . . . . . 6 class 𝑥
52, 4wcel 1436 . . . . 5 wff 1 ∈ 𝑥
6 vy . . . . . . . . 9 setvar 𝑦
76cv 1286 . . . . . . . 8 class 𝑦
8 caddc 7300 . . . . . . . 8 class +
97, 2, 8co 5615 . . . . . . 7 class (𝑦 + 1)
109, 4wcel 1436 . . . . . 6 wff (𝑦 + 1) ∈ 𝑥
1110, 6, 4wral 2355 . . . . 5 wff 𝑦𝑥 (𝑦 + 1) ∈ 𝑥
125, 11wa 102 . . . 4 wff (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)
1312, 3cab 2071 . . 3 class {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
1413cint 3673 . 2 class {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
151, 14wceq 1287 1 wff ℕ = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
Colors of variables: wff set class
This definition is referenced by:  dfnn2  8362
  Copyright terms: Public domain W3C validator