Theorem qnnen

Description: The rational numbers are countable. This proof does not use the Axiom of Choice, even though it uses an onto function, because the base set ( ZZ X. NN ) is numerable. Exercise 2 of Enderton p. 133. For purposes of the Metamath 100 list, we are considering Mario Carneiro's revision as the date this proof was completed. This is Metamath 100 proof #3. (Contributed by NM, 31-Jul-2004) (Revised by Mario Carneiro, 3-Mar-2013)

	Ref	Expression
Assertion	qnnen	⊢ ℚ ≈ ℕ

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		znnen	⊢ ℤ ≈ ℕ
7		ennum	⊢ ( ℤ ≈ ℕ → ( ℤ ∈ dom card ↔ ℕ ∈ dom card ) )
8	6 7	ax-mp	⊢ ( ℤ ∈ dom card ↔ ℕ ∈ dom card )
9	5 8	mpbir	⊢ ℤ ∈ dom card
10		xpnum	⊢ ( ( ℤ ∈ dom card ∧ ℕ ∈ dom card ) → ( ℤ × ℕ ) ∈ dom card )
11	9 5 10	mp2an	⊢ ( ℤ × ℕ ) ∈ dom card
12		eqid	⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ ↦ ( 𝑥 / 𝑦 ) ) = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ ↦ ( 𝑥 / 𝑦 ) )
13		ovex	⊢ ( 𝑥 / 𝑦 ) ∈ V
14	12 13	fnmpoi	⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ ↦ ( 𝑥 / 𝑦 ) ) Fn ( ℤ × ℕ )
15	12	rnmpo	⊢ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ ↦ ( 𝑥 / 𝑦 ) ) = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑧 = ( 𝑥 / 𝑦 ) }
16		elq	⊢ ( 𝑧 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑧 = ( 𝑥 / 𝑦 ) )
17	16	eqabi	⊢ ℚ = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑧 = ( 𝑥 / 𝑦 ) }
18	15 17	eqtr4i	⊢ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ ↦ ( 𝑥 / 𝑦 ) ) = ℚ
19		df-fo	⊢ ( ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ ↦ ( 𝑥 / 𝑦 ) ) : ( ℤ × ℕ ) –onto→ ℚ ↔ ( ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ ↦ ( 𝑥 / 𝑦 ) ) Fn ( ℤ × ℕ ) ∧ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ ↦ ( 𝑥 / 𝑦 ) ) = ℚ ) )
20	14 18 19	mpbir2an	⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ ↦ ( 𝑥 / 𝑦 ) ) : ( ℤ × ℕ ) –onto→ ℚ
21		fodomnum	⊢ ( ( ℤ × ℕ ) ∈ dom card → ( ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ ↦ ( 𝑥 / 𝑦 ) ) : ( ℤ × ℕ ) –onto→ ℚ → ℚ ≼ ( ℤ × ℕ ) ) )
22	11 20 21	mp2	⊢ ℚ ≼ ( ℤ × ℕ )
23		nnex	⊢ ℕ ∈ V
24	23	enref	⊢ ℕ ≈ ℕ
25		xpen	⊢ ( ( ℤ ≈ ℕ ∧ ℕ ≈ ℕ ) → ( ℤ × ℕ ) ≈ ( ℕ × ℕ ) )
26	6 24 25	mp2an	⊢ ( ℤ × ℕ ) ≈ ( ℕ × ℕ )
27		xpnnen	⊢ ( ℕ × ℕ ) ≈ ℕ
28	26 27	entri	⊢ ( ℤ × ℕ ) ≈ ℕ
29		domentr	⊢ ( ( ℚ ≼ ( ℤ × ℕ ) ∧ ( ℤ × ℕ ) ≈ ℕ ) → ℚ ≼ ℕ )
30	22 28 29	mp2an	⊢ ℚ ≼ ℕ
31		qex	⊢ ℚ ∈ V
32		nnssq	⊢ ℕ ⊆ ℚ
33		ssdomg	⊢ ( ℚ ∈ V → ( ℕ ⊆ ℚ → ℕ ≼ ℚ ) )
34	31 32 33	mp2	⊢ ℕ ≼ ℚ
35		sbth	⊢ ( ( ℚ ≼ ℕ ∧ ℕ ≼ ℚ ) → ℚ ≈ ℕ )
36	30 34 35	mp2an	⊢ ℚ ≈ ℕ