Metamath Proof Explorer

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 ⊢ x ∈ ℤ , y ∈ ℕ ⟼ x y = x ∈ ℤ , y ∈ ℕ ⟼ x y
13 ovex ⊢ x y ∈ V
14 12 13 fnmpoi ⊢ x ∈ ℤ , y ∈ ℕ ⟼ x y Fn ℤ × ℕ
15 12 rnmpo ⊢ ran ⁡ x ∈ ℤ , y ∈ ℕ ⟼ x y = z | ∃ x ∈ ℤ ∃ y ∈ ℕ z = x y
16 elq ⊢ z ∈ ℚ ↔ ∃ x ∈ ℤ ∃ y ∈ ℕ z = x y
17 16 abbi2i ⊢ ℚ = z | ∃ x ∈ ℤ ∃ y ∈ ℕ z = x y
18 15 17 eqtr4i ⊢ ran ⁡ x ∈ ℤ , y ∈ ℕ ⟼ x y = ℚ
19 df-fo ⊢ x ∈ ℤ , y ∈ ℕ ⟼ x y : ℤ × ℕ ⟶ onto ℚ ↔ x ∈ ℤ , y ∈ ℕ ⟼ x y Fn ℤ × ℕ ∧ ran ⁡ x ∈ ℤ , y ∈ ℕ ⟼ x y = ℚ
20 14 18 19 mpbir2an ⊢ x ∈ ℤ , y ∈ ℕ ⟼ x y : ℤ × ℕ ⟶ onto ℚ
21 fodomnum ⊢ ℤ × ℕ ∈ dom ⁡ card → x ∈ ℤ , y ∈ ℕ ⟼ x y : ℤ × ℕ ⟶ 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 ⊢ ℚ ≈ ℕ