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∈xy+1∈x

Proof

Step Hyp Ref Expression
1 1ex ⊢1∈V
2 1 elintab ⊢1∈⋂x|1∈x∧∀y∈xy+1∈x↔∀x1∈x∧∀y∈xy+1∈x→1∈x
3 simpl ⊢1∈x∧∀y∈xy+1∈x→1∈x
4 2 3 mpgbir ⊢1∈⋂x|1∈x∧∀y∈xy+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∈xy+1∈x→z∈x→z+1∈x
8 7 adantl ⊢1∈x∧∀y∈xy+1∈x→z∈x→z+1∈x
9 8 a2i ⊢1∈x∧∀y∈xy+1∈x→z∈x→1∈x∧∀y∈xy+1∈x→z+1∈x
10 9 alimi ⊢∀x1∈x∧∀y∈xy+1∈x→z∈x→∀x1∈x∧∀y∈xy+1∈x→z+1∈x
11 vex ⊢z∈V
12 11 elintab ⊢z∈⋂x|1∈x∧∀y∈xy+1∈x↔∀x1∈x∧∀y∈xy+1∈x→z∈x
13 ovex ⊢z+1∈V
14 13 elintab ⊢z+1∈⋂x|1∈x∧∀y∈xy+1∈x↔∀x1∈x∧∀y∈xy+1∈x→z+1∈x
15 10 12 14 3imtr4i ⊢z∈⋂x|1∈x∧∀y∈xy+1∈x→z+1∈⋂x|1∈x∧∀y∈xy+1∈x
16 15 rgen ⊢∀z∈⋂x|1∈x∧∀y∈xy+1∈xz+1∈⋂x|1∈x∧∀y∈xy+1∈x
17 peano5nni ⊢1∈⋂x|1∈x∧∀y∈xy+1∈x∧∀z∈⋂x|1∈x∧∀y∈xy+1∈xz+1∈⋂x|1∈x∧∀y∈xy+1∈x→ℕ⊆⋂x|1∈x∧∀y∈xy+1∈x
18 4 16 17 mp2an ⊢ℕ⊆⋂x|1∈x∧∀y∈xy+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∈xy+1∈x↔∀y∈ℕy+1∈ℕ
26 23 25 anbi12d ⊢x=ℕ→1∈x∧∀y∈xy+1∈x↔1∈ℕ∧∀y∈ℕy+1∈ℕ
27 22 26 elab ⊢ℕ∈x|1∈x∧∀y∈xy+1∈x↔1∈ℕ∧∀y∈ℕy+1∈ℕ
28 19 21 27 mpbir2an ⊢ℕ∈x|1∈x∧∀y∈xy+1∈x
29 intss1 ⊢ℕ∈x|1∈x∧∀y∈xy+1∈x→⋂x|1∈x∧∀y∈xy+1∈x⊆ℕ
30 28 29 ax-mp ⊢⋂x|1∈x∧∀y∈xy+1∈x⊆ℕ
31 18 30 eqssi ⊢ℕ=⋂x|1∈x∧∀y∈xy+1∈x