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 ⊢ ( 𝑥 ∈ ℤ ↔ ∃ 𝑦 ∈ ℕ ∃ 𝑧 ∈ ℕ 𝑥 = ( 𝑦 − 𝑧 ) )
2 subf ⊢ − : ( ℂ × ℂ ) ⟶ ℂ
3 ffn ⊢ ( − : ( ℂ × ℂ ) ⟶ ℂ → − Fn ( ℂ × ℂ ) )
4 2 3 ax-mp ⊢ − Fn ( ℂ × ℂ )
5 nnsscn ⊢ ℕ ⊆ ℂ
6 xpss12 ⊢ ( ( ℕ ⊆ ℂ ∧ ℕ ⊆ ℂ ) → ( ℕ × ℕ ) ⊆ ( ℂ × ℂ ) )
7 5 5 6 mp2an ⊢ ( ℕ × ℕ ) ⊆ ( ℂ × ℂ )
8 ovelimab ⊢ ( ( − Fn ( ℂ × ℂ ) ∧ ( ℕ × ℕ ) ⊆ ( ℂ × ℂ ) ) → ( 𝑥 ∈ ( − “ ( ℕ × ℕ ) ) ↔ ∃ 𝑦 ∈ ℕ ∃ 𝑧 ∈ ℕ 𝑥 = ( 𝑦 − 𝑧 ) ) )
9 4 7 8 mp2an ⊢ ( 𝑥 ∈ ( − “ ( ℕ × ℕ ) ) ↔ ∃ 𝑦 ∈ ℕ ∃ 𝑧 ∈ ℕ 𝑥 = ( 𝑦 − 𝑧 ) )
10 1 9 bitr4i ⊢ ( 𝑥 ∈ ℤ ↔ 𝑥 ∈ ( − “ ( ℕ × ℕ ) ) )
11 10 eqriv ⊢ ℤ = ( − “ ( ℕ × ℕ ) )