qdensere

Description: QQ is dense in the standard topology on RR . (Contributed by NM, 1-Mar-2007)

		Ref	Expression
	Assertion	qdensere	$⊢ cls (topGen (ran (.))) (ℚ) = ℝ$

Proof

Step	Hyp	Ref	Expression
1		retop	$⊢ topGen (ran (.)) \in Top$
2		qssre	$⊢ ℚ \subseteq ℝ$
3		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
4	3	clsss3	$⊢ (topGen (ran (.)) \in Top \land ℚ \subseteq ℝ) \to cls (topGen (ran (.))) (ℚ) \subseteq ℝ$
5	1 2 4	mp2an	$⊢ cls (topGen (ran (.))) (ℚ) \subseteq ℝ$
6		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
7		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
8		ovelrn	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \to (y \in ran (.) \leftrightarrow \exists z \in ℝ^{} \exists w \in ℝ^{} y = (z, w))$
9	6 7 8	mp2b	$⊢ y \in ran (.) \leftrightarrow \exists z \in ℝ^{} \exists w \in ℝ^{} y = (z, w)$
10		elioo3g	$⊢ x \in (z, w) \leftrightarrow ((z \in ℝ^{} \land w \in ℝ^{} \land x \in ℝ^{*}) \land (z < x \land x < w))$
11	10	simplbi	$⊢ x \in (z, w) \to (z \in ℝ^{} \land w \in ℝ^{} \land x \in ℝ^{*})$
12	11	simp1d	$⊢ x \in (z, w) \to z \in ℝ^{*}$
13	12	ad2antrr	$⊢ ((x \in (z, w) \land y \in ℚ) \land (z < y \land y < w)) \to z \in ℝ^{*}$
14	11	simp2d	$⊢ x \in (z, w) \to w \in ℝ^{*}$
15	14	ad2antrr	$⊢ ((x \in (z, w) \land y \in ℚ) \land (z < y \land y < w)) \to w \in ℝ^{*}$
16		qre	$⊢ y \in ℚ \to y \in ℝ$
17	16	ad2antlr	$⊢ ((x \in (z, w) \land y \in ℚ) \land (z < y \land y < w)) \to y \in ℝ$
18	17	rexrd	$⊢ ((x \in (z, w) \land y \in ℚ) \land (z < y \land y < w)) \to y \in ℝ^{*}$
19	13 15 18	3jca	$⊢ ((x \in (z, w) \land y \in ℚ) \land (z < y \land y < w)) \to (z \in ℝ^{} \land w \in ℝ^{} \land y \in ℝ^{*})$
20		simpr	$⊢ ((x \in (z, w) \land y \in ℚ) \land (z < y \land y < w)) \to (z < y \land y < w)$
21		elioo3g	$⊢ y \in (z, w) \leftrightarrow ((z \in ℝ^{} \land w \in ℝ^{} \land y \in ℝ^{*}) \land (z < y \land y < w))$
22	19 20 21	sylanbrc	$⊢ ((x \in (z, w) \land y \in ℚ) \land (z < y \land y < w)) \to y \in (z, w)$
23		simplr	$⊢ ((x \in (z, w) \land y \in ℚ) \land (z < y \land y < w)) \to y \in ℚ$
24		inelcm	$⊢ (y \in (z, w) \land y \in ℚ) \to (z, w) \cap ℚ \neq \emptyset$
25	22 23 24	syl2anc	$⊢ ((x \in (z, w) \land y \in ℚ) \land (z < y \land y < w)) \to (z, w) \cap ℚ \neq \emptyset$
26	11	simp3d	$⊢ x \in (z, w) \to x \in ℝ^{*}$
27		eliooord	$⊢ x \in (z, w) \to (z < x \land x < w)$
28	27	simpld	$⊢ x \in (z, w) \to z < x$
29	27	simprd	$⊢ x \in (z, w) \to x < w$
30	12 26 14 28 29	xrlttrd	$⊢ x \in (z, w) \to z < w$
31		qbtwnxr	$⊢ (z \in ℝ^{} \land w \in ℝ^{} \land z < w) \to \exists y \in ℚ (z < y \land y < w)$
32	12 14 30 31	syl3anc	$⊢ x \in (z, w) \to \exists y \in ℚ (z < y \land y < w)$
33	25 32	r19.29a	$⊢ x \in (z, w) \to (z, w) \cap ℚ \neq \emptyset$
34	33	a1i	$⊢ y = (z, w) \to (x \in (z, w) \to (z, w) \cap ℚ \neq \emptyset)$
35		eleq2	$⊢ y = (z, w) \to (x \in y \leftrightarrow x \in (z, w))$
36		ineq1	$⊢ y = (z, w) \to y \cap ℚ = (z, w) \cap ℚ$
37	36	neeq1d	$⊢ y = (z, w) \to (y \cap ℚ \neq \emptyset \leftrightarrow (z, w) \cap ℚ \neq \emptyset)$
38	34 35 37	3imtr4d	$⊢ y = (z, w) \to (x \in y \to y \cap ℚ \neq \emptyset)$
39	38	rexlimivw	$⊢ \exists w \in ℝ^{*} y = (z, w) \to (x \in y \to y \cap ℚ \neq \emptyset)$
40	39	rexlimivw	$⊢ \exists z \in ℝ^{} \exists w \in ℝ^{} y = (z, w) \to (x \in y \to y \cap ℚ \neq \emptyset)$
41	9 40	sylbi	$⊢ y \in ran (.) \to (x \in y \to y \cap ℚ \neq \emptyset)$
42	41	rgen	$⊢ \forall y \in ran (.) (x \in y \to y \cap ℚ \neq \emptyset)$
43		eqidd	$⊢ x \in ℝ \to topGen (ran (.)) = topGen (ran (.))$
44	3	a1i	$⊢ x \in ℝ \to ℝ = ⋃ topGen (ran (.))$
45		retopbas	$⊢ ran (.) \in TopBases$
46	45	a1i	$⊢ x \in ℝ \to ran (.) \in TopBases$
47	2	a1i	$⊢ x \in ℝ \to ℚ \subseteq ℝ$
48		id	$⊢ x \in ℝ \to x \in ℝ$
49	43 44 46 47 48	elcls3	$⊢ x \in ℝ \to (x \in cls (topGen (ran (.))) (ℚ) \leftrightarrow \forall y \in ran (.) (x \in y \to y \cap ℚ \neq \emptyset))$
50	42 49	mpbiri	$⊢ x \in ℝ \to x \in cls (topGen (ran (.))) (ℚ)$
51	50	ssriv	$⊢ ℝ \subseteq cls (topGen (ran (.))) (ℚ)$
52	5 51	eqssi	$⊢ cls (topGen (ran (.))) (ℚ) = ℝ$

Metamath Proof Explorer

Theorem qdensere

Proof