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	⊢ ℤ = ( − “ ( ℕ × ℕ ) )