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∈xy+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∈xy+1∈x↔∀y∈zy+1∈z
4 1 3 anbi12d ⊢x=z→1∈x∧∀y∈xy+1∈x↔1∈z∧∀y∈zy+1∈z
5 dfnn2 ⊢ℕ=⋂z|1∈z∧∀y∈zy+1∈z
6 5 eqeq2i ⊢x=ℕ↔x=⋂z|1∈z∧∀y∈zy+1∈z
7 eleq2 ⊢x=ℕ→1∈x↔1∈ℕ
8 eleq2 ⊢x=ℕ→y+1∈x↔y+1∈ℕ
9 8 raleqbi1dv ⊢x=ℕ→∀y∈xy+1∈x↔∀y∈ℕy+1∈ℕ
10 7 9 anbi12d ⊢x=ℕ→1∈x∧∀y∈xy+1∈x↔1∈ℕ∧∀y∈ℕy+1∈ℕ
11 6 10 sylbir ⊢x=⋂z|1∈z∧∀y∈zy+1∈z→1∈x∧∀y∈xy+1∈x↔1∈ℕ∧∀y∈ℕy+1∈ℕ
12 nnssre ⊢ℕ⊆ℝ
13 5 12 eqsstrri ⊢⋂z|1∈z∧∀y∈zy+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∈zy+1∈z⊆ℝ∧1∈ℕ∧∀y∈ℕy+1∈ℕ
19 4 11 18 intabs ⊢⋂x|x⊆ℝ∧1∈x∧∀y∈xy+1∈x=⋂x|1∈x∧∀y∈xy+1∈x
20 3anass ⊢x⊆ℝ∧1∈x∧∀y∈xy+1∈x↔x⊆ℝ∧1∈x∧∀y∈xy+1∈x
21 20 abbii ⊢x|x⊆ℝ∧1∈x∧∀y∈xy+1∈x=x|x⊆ℝ∧1∈x∧∀y∈xy+1∈x
22 21 inteqi ⊢⋂x|x⊆ℝ∧1∈x∧∀y∈xy+1∈x=⋂x|x⊆ℝ∧1∈x∧∀y∈xy+1∈x
23 dfnn2 ⊢ℕ=⋂x|1∈x∧∀y∈xy+1∈x
24 19 22 23 3eqtr4ri ⊢ℕ=⋂x|x⊆ℝ∧1∈x∧∀y∈xy+1∈x