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	⊢ ℤ ≈ ℕ