Metamath Proof Explorer

Theorem dfnn2

Description: Alternate definition of the set of positive integers. This was our original definition, before the current df-nn replaced it. This definition requires the axiom of infinity to ensure it has the properties we expect. (Contributed by Jeff Hankins, 12-Sep-2013) (Revised by Mario Carneiro, 3-May-2014)

Ref Expression
Assertion dfnn2 ⊢ ℕ = ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x

Proof

Step Hyp Ref Expression
1 1ex ⊢ 1 ∈ V
2 1 elintab ⊢ 1 ∈ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ↔ ∀ x 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → 1 ∈ x
3 simpl ⊢ 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → 1 ∈ x
4 2 3 mpgbir ⊢ 1 ∈ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x
5 oveq1 ⊢ y = z → y + 1 = z + 1
6 5 eleq1d ⊢ y = z → y + 1 ∈ x ↔ z + 1 ∈ x
7 6 rspccv ⊢ ∀ y ∈ x y + 1 ∈ x → z ∈ x → z + 1 ∈ x
8 7 adantl ⊢ 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → z ∈ x → z + 1 ∈ x
9 8 a2i ⊢ 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → z ∈ x → 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → z + 1 ∈ x
10 9 alimi ⊢ ∀ x 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → z ∈ x → ∀ x 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → z + 1 ∈ x
11 vex ⊢ z ∈ V
12 11 elintab ⊢ z ∈ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ↔ ∀ x 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → z ∈ x
13 ovex ⊢ z + 1 ∈ V
14 13 elintab ⊢ z + 1 ∈ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ↔ ∀ x 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → z + 1 ∈ x
15 10 12 14 3imtr4i ⊢ z ∈ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → z + 1 ∈ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x
16 15 rgen ⊢ ∀ z ∈ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x z + 1 ∈ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x
17 peano5nni ⊢ 1 ∈ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ∧ ∀ z ∈ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x z + 1 ∈ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → ℕ ⊆ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x
18 4 16 17 mp2an ⊢ ℕ ⊆ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x
19 1nn ⊢ 1 ∈ ℕ
20 peano2nn ⊢ y ∈ ℕ → y + 1 ∈ ℕ
21 20 rgen ⊢ ∀ y ∈ ℕ y + 1 ∈ ℕ
22 nnex ⊢ ℕ ∈ V
23 eleq2 ⊢ x = ℕ → 1 ∈ x ↔ 1 ∈ ℕ
24 eleq2 ⊢ x = ℕ → y + 1 ∈ x ↔ y + 1 ∈ ℕ
25 24 raleqbi1dv ⊢ x = ℕ → ∀ y ∈ x y + 1 ∈ x ↔ ∀ y ∈ ℕ y + 1 ∈ ℕ
26 23 25 anbi12d ⊢ x = ℕ → 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ↔ 1 ∈ ℕ ∧ ∀ y ∈ ℕ y + 1 ∈ ℕ
27 22 26 elab ⊢ ℕ ∈ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ↔ 1 ∈ ℕ ∧ ∀ y ∈ ℕ y + 1 ∈ ℕ
28 19 21 27 mpbir2an ⊢ ℕ ∈ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x
29 intss1 ⊢ ℕ ∈ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x → ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ⊆ ℕ
30 28 29 ax-mp ⊢ ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x ⊆ ℕ
31 18 30 eqssi ⊢ ℕ = ⋂ x | 1 ∈ x ∧ ∀ y ∈ x y + 1 ∈ x