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

Metamath Proof Explorer

Theorem znnen

Description: The set of integers and the set of positive integers are equinumerous. Exercise 1 of Gleason p. 140. (Contributed by NM, 31-Jul-2004) (Proof shortened by Mario Carneiro, 13-Jun-2014)

Ref Expression
Assertion znnen ℤ ≈ ℕ

Proof

Step Hyp Ref Expression
1 omelon ⊢ ω ∈ On
2 nnenom ⊢ ℕ ≈ ω
3 2 ensymi ⊢ ω ≈ ℕ
4 isnumi ⊢ ( ( ω ∈ On ∧ ω ≈ ℕ ) → ℕ ∈ dom card )
5 1 3 4 mp2an ⊢ ℕ ∈ dom card
6 xpnum ⊢ ( ( ℕ ∈ dom card ∧ ℕ ∈ dom card ) → ( ℕ × ℕ ) ∈ dom card )
7 5 5 6 mp2an ⊢ ( ℕ × ℕ ) ∈ dom card
8 subf ⊢ − : ( ℂ × ℂ ) ⟶ ℂ
9 ffun ⊢ ( − : ( ℂ × ℂ ) ⟶ ℂ → Fun − )
10 8 9 ax-mp ⊢ Fun −
11 nnsscn ⊢ ℕ ⊆ ℂ
12 xpss12 ⊢ ( ( ℕ ⊆ ℂ ∧ ℕ ⊆ ℂ ) → ( ℕ × ℕ ) ⊆ ( ℂ × ℂ ) )
13 11 11 12 mp2an ⊢ ( ℕ × ℕ ) ⊆ ( ℂ × ℂ )
14 8 fdmi ⊢ dom − = ( ℂ × ℂ )
15 13 14 sseqtrri ⊢ ( ℕ × ℕ ) ⊆ dom −
16 fores ⊢ ( ( Fun − ∧ ( ℕ × ℕ ) ⊆ dom − ) → ( − ↾ ( ℕ × ℕ ) ) : ( ℕ × ℕ ) –onto→ ( − “ ( ℕ × ℕ ) ) )
17 10 15 16 mp2an ⊢ ( − ↾ ( ℕ × ℕ ) ) : ( ℕ × ℕ ) –onto→ ( − “ ( ℕ × ℕ ) )
18 dfz2 ⊢ ℤ = ( − “ ( ℕ × ℕ ) )
19 foeq3 ⊢ ( ℤ = ( − “ ( ℕ × ℕ ) ) → ( ( − ↾ ( ℕ × ℕ ) ) : ( ℕ × ℕ ) –onto→ ℤ ↔ ( − ↾ ( ℕ × ℕ ) ) : ( ℕ × ℕ ) –onto→ ( − “ ( ℕ × ℕ ) ) ) )
20 18 19 ax-mp ⊢ ( ( − ↾ ( ℕ × ℕ ) ) : ( ℕ × ℕ ) –onto→ ℤ ↔ ( − ↾ ( ℕ × ℕ ) ) : ( ℕ × ℕ ) –onto→ ( − “ ( ℕ × ℕ ) ) )
21 17 20 mpbir ⊢ ( − ↾ ( ℕ × ℕ ) ) : ( ℕ × ℕ ) –onto→ ℤ
22 fodomnum ⊢ ( ( ℕ × ℕ ) ∈ dom card → ( ( − ↾ ( ℕ × ℕ ) ) : ( ℕ × ℕ ) –onto→ ℤ → ℤ ≼ ( ℕ × ℕ ) ) )
23 7 21 22 mp2 ⊢ ℤ ≼ ( ℕ × ℕ )
24 xpnnen ⊢ ( ℕ × ℕ ) ≈ ℕ
25 domentr ⊢ ( ( ℤ ≼ ( ℕ × ℕ ) ∧ ( ℕ × ℕ ) ≈ ℕ ) → ℤ ≼ ℕ )
26 23 24 25 mp2an ⊢ ℤ ≼ ℕ
27 zex ⊢ ℤ ∈ V
28 nnssz ⊢ ℕ ⊆ ℤ
29 ssdomg ⊢ ( ℤ ∈ V → ( ℕ ⊆ ℤ → ℕ ≼ ℤ ) )
30 27 28 29 mp2 ⊢ ℕ ≼ ℤ
31 sbth ⊢ ( ( ℤ ≼ ℕ ∧ ℕ ≼ ℤ ) → ℤ ≈ ℕ )
32 26 30 31 mp2an ⊢ ℤ ≈ ℕ