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

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 ⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ ↦ ( 𝑥 / 𝑦 ) ) = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ ↦ ( 𝑥 / 𝑦 ) )
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 ⊢ ℚ ≈ ℕ