This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Integer sets Integers (as a subset of complex numbers) zexALT
Description: Alternate proof of zex . (Contributed by NM , 30-Jul-2004) (Revised by Mario Carneiro , 16-May-2014) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Assertion
zexALT ⊢ ℤ ∈ V
Proof
Step
Hyp
Ref
Expression
1
dfz2 ⊢ ℤ = ( − “ ( ℕ × ℕ ) )
2
subf ⊢ − : ( ℂ × ℂ ) ⟶ ℂ
3
ffun ⊢ ( − : ( ℂ × ℂ ) ⟶ ℂ → Fun − )
4
nnexALT ⊢ ℕ ∈ V
5
4 4
xpex ⊢ ( ℕ × ℕ ) ∈ V
6
5
funimaex ⊢ ( Fun − → ( − “ ( ℕ × ℕ ) ) ∈ V )
7
2 3 6
mp2b ⊢ ( − “ ( ℕ × ℕ ) ) ∈ V
8
1 7
eqeltri ⊢ ℤ ∈ V