This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfz2

Description: Alternative definition of the integers, based on elz2 . (Contributed by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion dfz2 ⊢ ℤ = − ℕ × ℕ

Proof

Step Hyp Ref Expression
1 elz2 ⊢ x ∈ ℤ ↔ ∃ y ∈ ℕ ∃ z ∈ ℕ x = y − z
2 subf ⊢ − : ℂ × ℂ ⟶ ℂ
3 ffn ⊢ − : ℂ × ℂ ⟶ ℂ → − Fn ℂ × ℂ
4 2 3 ax-mp ⊢ − Fn ℂ × ℂ
5 nnsscn ⊢ ℕ ⊆ ℂ
6 xpss12 ⊢ ℕ ⊆ ℂ ∧ ℕ ⊆ ℂ → ℕ × ℕ ⊆ ℂ × ℂ
7 5 5 6 mp2an ⊢ ℕ × ℕ ⊆ ℂ × ℂ
8 ovelimab ⊢ − Fn ℂ × ℂ ∧ ℕ × ℕ ⊆ ℂ × ℂ → x ∈ − ℕ × ℕ ↔ ∃ y ∈ ℕ ∃ z ∈ ℕ x = y − z
9 4 7 8 mp2an ⊢ x ∈ − ℕ × ℕ ↔ ∃ y ∈ ℕ ∃ z ∈ ℕ x = y − z
10 1 9 bitr4i ⊢ x ∈ ℤ ↔ x ∈ − ℕ × ℕ
11 10 eqriv ⊢ ℤ = − ℕ × ℕ