Metamath Proof Explorer

Theorem dfnn3

Description: Alternate definition of the set of positive integers. Definition of positive integers in Apostol p. 22. (Contributed by NM, 3-Jul-2005)

Ref Expression
Assertion dfnn3 ⊢ ℕ = ⋂ x | x ⊆ ℝ ∧ 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ x = z → 1 ∈ x ↔ 1 ∈ z
2 eleq2 ⊢ x = z → y + 1 ∈ x ↔ y + 1 ∈ z
3 2 raleqbi1dv ⊢ x = z → ∀ y ∈ x y + 1 ∈ x ↔ ∀ y ∈ z y + 1 ∈ z
4 1 3 anbi12d ⊢ x = z → 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ↔ 1 ∈ z ∧ ∀ y ∈ z y + 1 ∈ z
5 dfnn2 ⊢ ℕ = ⋂ z | 1 ∈ z ∧ ∀ y ∈ z y + 1 ∈ z
6 5 eqeq2i ⊢ x = ℕ ↔ x = ⋂ z | 1 ∈ z ∧ ∀ y ∈ z y + 1 ∈ z
7 eleq2 ⊢ x = ℕ → 1 ∈ x ↔ 1 ∈ ℕ
8 eleq2 ⊢ x = ℕ → y + 1 ∈ x ↔ y + 1 ∈ ℕ
9 8 raleqbi1dv ⊢ x = ℕ → ∀ y ∈ x y + 1 ∈ x ↔ ∀ y ∈ ℕ y + 1 ∈ ℕ
10 7 9 anbi12d ⊢ x = ℕ → 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ↔ 1 ∈ ℕ ∧ ∀ y ∈ ℕ y + 1 ∈ ℕ
11 6 10 sylbir ⊢ x = ⋂ z | 1 ∈ z ∧ ∀ y ∈ z y + 1 ∈ z → 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ↔ 1 ∈ ℕ ∧ ∀ y ∈ ℕ y + 1 ∈ ℕ
12 nnssre ⊢ ℕ ⊆ ℝ
13 5 12 eqsstrri ⊢ ⋂ z | 1 ∈ z ∧ ∀ y ∈ z y + 1 ∈ z ⊆ ℝ
14 1nn ⊢ 1 ∈ ℕ
15 peano2nn ⊢ y ∈ ℕ → y + 1 ∈ ℕ
16 15 rgen ⊢ ∀ y ∈ ℕ y + 1 ∈ ℕ
17 14 16 pm3.2i ⊢ 1 ∈ ℕ ∧ ∀ y ∈ ℕ y + 1 ∈ ℕ
18 13 17 pm3.2i ⊢ ⋂ z | 1 ∈ z ∧ ∀ y ∈ z y + 1 ∈ z ⊆ ℝ ∧ 1 ∈ ℕ ∧ ∀ y ∈ ℕ y + 1 ∈ ℕ
19 4 11 18 intabs ⊢ ⋂ x | x ⊆ ℝ ∧ 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x = ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x
20 3anass ⊢ x ⊆ ℝ ∧ 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ↔ x ⊆ ℝ ∧ 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x
21 20 abbii ⊢ x | x ⊆ ℝ ∧ 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x = x | x ⊆ ℝ ∧ 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x
22 21 inteqi ⊢ ⋂ x | x ⊆ ℝ ∧ 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x = ⋂ x | x ⊆ ℝ ∧ 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x
23 dfnn2 ⊢ ℕ = ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x
24 19 22 23 3eqtr4ri ⊢ ℕ = ⋂ x | x ⊆ ℝ ∧ 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x