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	$⊢ ℚ \approx ℕ$

Proof

Step	Hyp	Ref	Expression
1		omelon	$⊢ ω \in On$
2		nnenom	$⊢ ℕ \approx ω$
3	2	ensymi	$⊢ ω \approx ℕ$
4		isnumi	$⊢ (ω \in On \land ω \approx ℕ) \to ℕ \in dom card$
5	1 3 4	mp2an	$⊢ ℕ \in dom card$
6		znnen	$⊢ ℤ \approx ℕ$
7		ennum	$⊢ ℤ \approx ℕ \to (ℤ \in dom card \leftrightarrow ℕ \in dom card)$
8	6 7	ax-mp	$⊢ ℤ \in dom card \leftrightarrow ℕ \in dom card$
9	5 8	mpbir	$⊢ ℤ \in dom card$
10		xpnum	$⊢ (ℤ \in dom card \land ℕ \in dom card) \to ℤ \times ℕ \in dom card$
11	9 5 10	mp2an	$⊢ ℤ \times ℕ \in dom card$
12		eqid	$⊢ (x \in ℤ, y \in ℕ ⟼ \frac{x}{y}) = (x \in ℤ, y \in ℕ ⟼ \frac{x}{y})$
13		ovex	$⊢ \frac{x}{y} \in V$
14	12 13	fnmpoi	$⊢ (x \in ℤ, y \in ℕ ⟼ \frac{x}{y}) Fn (ℤ \times ℕ)$
15	12	rnmpo	$⊢ ran (x \in ℤ, y \in ℕ ⟼ \frac{x}{y}) = \{z \| \exists x \in ℤ \exists y \in ℕ z = \frac{x}{y}\}$
16		elq	$⊢ z \in ℚ \leftrightarrow \exists x \in ℤ \exists y \in ℕ z = \frac{x}{y}$
17	16	eqabi	$⊢ ℚ = \{z \| \exists x \in ℤ \exists y \in ℕ z = \frac{x}{y}\}$
18	15 17	eqtr4i	$⊢ ran (x \in ℤ, y \in ℕ ⟼ \frac{x}{y}) = ℚ$
19		df-fo	$⊢ (x \in ℤ, y \in ℕ ⟼ \frac{x}{y}) : ℤ \times ℕ \underset{onto}{⟶} ℚ \leftrightarrow ((x \in ℤ, y \in ℕ ⟼ \frac{x}{y}) Fn (ℤ \times ℕ) \land ran (x \in ℤ, y \in ℕ ⟼ \frac{x}{y}) = ℚ)$
20	14 18 19	mpbir2an	$⊢ (x \in ℤ, y \in ℕ ⟼ \frac{x}{y}) : ℤ \times ℕ \underset{onto}{⟶} ℚ$
21		fodomnum	$⊢ ℤ \times ℕ \in dom card \to ((x \in ℤ, y \in ℕ ⟼ \frac{x}{y}) : ℤ \times ℕ \underset{onto}{⟶} ℚ \to ℚ ≼ (ℤ \times ℕ))$
22	11 20 21	mp2	$⊢ ℚ ≼ (ℤ \times ℕ)$
23		nnex	$⊢ ℕ \in V$
24	23	enref	$⊢ ℕ \approx ℕ$
25		xpen	$⊢ (ℤ \approx ℕ \land ℕ \approx ℕ) \to (ℤ \times ℕ) \approx (ℕ \times ℕ)$
26	6 24 25	mp2an	$⊢ (ℤ \times ℕ) \approx (ℕ \times ℕ)$
27		xpnnen	$⊢ (ℕ \times ℕ) \approx ℕ$
28	26 27	entri	$⊢ (ℤ \times ℕ) \approx ℕ$
29		domentr	$⊢ (ℚ ≼ (ℤ \times ℕ) \land (ℤ \times ℕ) \approx ℕ) \to ℚ ≼ ℕ$
30	22 28 29	mp2an	$⊢ ℚ ≼ ℕ$
31		qex	$⊢ ℚ \in V$
32		nnssq	$⊢ ℕ \subseteq ℚ$
33		ssdomg	$⊢ ℚ \in V \to (ℕ \subseteq ℚ \to ℕ ≼ ℚ)$
34	31 32 33	mp2	$⊢ ℕ ≼ ℚ$
35		sbth	$⊢ (ℚ ≼ ℕ \land ℕ ≼ ℚ) \to ℚ \approx ℕ$
36	30 34 35	mp2an	$⊢ ℚ \approx ℕ$

Metamath Proof Explorer

Theorem qnnen

Proof