Theorem 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 (,) ) ∈ Top
2		qssre	⊢ ℚ ⊆ ℝ
3		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
4	3	clsss3	⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ℚ ⊆ ℝ ) → ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) ⊆ ℝ )
5	1 2 4	mp2an	⊢ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) ⊆ ℝ
6		ioof	⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
7		ffn	⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
8		ovelrn	⊢ ( (,) Fn ( ℝ* × ℝ* ) → ( 𝑦 ∈ ran (,) ↔ ∃ 𝑧 ∈ ℝ* ∃ 𝑤 ∈ ℝ* 𝑦 = ( 𝑧 (,) 𝑤 ) ) )
9	6 7 8	mp2b	⊢ ( 𝑦 ∈ ran (,) ↔ ∃ 𝑧 ∈ ℝ* ∃ 𝑤 ∈ ℝ* 𝑦 = ( 𝑧 (,) 𝑤 ) )
10		elioo3g	⊢ ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) ↔ ( ( 𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) ∧ ( 𝑧 < 𝑥 ∧ 𝑥 < 𝑤 ) ) )
11	10	simplbi	⊢ ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) → ( 𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) )
12	11	simp1d	⊢ ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) → 𝑧 ∈ ℝ* )
13	12	ad2antrr	⊢ ( ( ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) ∧ 𝑦 ∈ ℚ ) ∧ ( 𝑧 < 𝑦 ∧ 𝑦 < 𝑤 ) ) → 𝑧 ∈ ℝ* )
14	11	simp2d	⊢ ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) → 𝑤 ∈ ℝ* )
15	14	ad2antrr	⊢ ( ( ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) ∧ 𝑦 ∈ ℚ ) ∧ ( 𝑧 < 𝑦 ∧ 𝑦 < 𝑤 ) ) → 𝑤 ∈ ℝ* )
16		qre	⊢ ( 𝑦 ∈ ℚ → 𝑦 ∈ ℝ )
17	16	ad2antlr	⊢ ( ( ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) ∧ 𝑦 ∈ ℚ ) ∧ ( 𝑧 < 𝑦 ∧ 𝑦 < 𝑤 ) ) → 𝑦 ∈ ℝ )
18	17	rexrd	⊢ ( ( ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) ∧ 𝑦 ∈ ℚ ) ∧ ( 𝑧 < 𝑦 ∧ 𝑦 < 𝑤 ) ) → 𝑦 ∈ ℝ* )
19	13 15 18	3jca	⊢ ( ( ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) ∧ 𝑦 ∈ ℚ ) ∧ ( 𝑧 < 𝑦 ∧ 𝑦 < 𝑤 ) ) → ( 𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) )
20		simpr	⊢ ( ( ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) ∧ 𝑦 ∈ ℚ ) ∧ ( 𝑧 < 𝑦 ∧ 𝑦 < 𝑤 ) ) → ( 𝑧 < 𝑦 ∧ 𝑦 < 𝑤 ) )
21		elioo3g	⊢ ( 𝑦 ∈ ( 𝑧 (,) 𝑤 ) ↔ ( ( 𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑧 < 𝑦 ∧ 𝑦 < 𝑤 ) ) )
22	19 20 21	sylanbrc	⊢ ( ( ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) ∧ 𝑦 ∈ ℚ ) ∧ ( 𝑧 < 𝑦 ∧ 𝑦 < 𝑤 ) ) → 𝑦 ∈ ( 𝑧 (,) 𝑤 ) )
23		simplr	⊢ ( ( ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) ∧ 𝑦 ∈ ℚ ) ∧ ( 𝑧 < 𝑦 ∧ 𝑦 < 𝑤 ) ) → 𝑦 ∈ ℚ )
24		inelcm	⊢ ( ( 𝑦 ∈ ( 𝑧 (,) 𝑤 ) ∧ 𝑦 ∈ ℚ ) → ( ( 𝑧 (,) 𝑤 ) ∩ ℚ ) ≠ ∅ )
25	22 23 24	syl2anc	⊢ ( ( ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) ∧ 𝑦 ∈ ℚ ) ∧ ( 𝑧 < 𝑦 ∧ 𝑦 < 𝑤 ) ) → ( ( 𝑧 (,) 𝑤 ) ∩ ℚ ) ≠ ∅ )
26	11	simp3d	⊢ ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) → 𝑥 ∈ ℝ* )
27		eliooord	⊢ ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) → ( 𝑧 < 𝑥 ∧ 𝑥 < 𝑤 ) )
28	27	simpld	⊢ ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) → 𝑧 < 𝑥 )
29	27	simprd	⊢ ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) → 𝑥 < 𝑤 )
30	12 26 14 28 29	xrlttrd	⊢ ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) → 𝑧 < 𝑤 )
31		qbtwnxr	⊢ ( ( 𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ∧ 𝑧 < 𝑤 ) → ∃ 𝑦 ∈ ℚ ( 𝑧 < 𝑦 ∧ 𝑦 < 𝑤 ) )
32	12 14 30 31	syl3anc	⊢ ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) → ∃ 𝑦 ∈ ℚ ( 𝑧 < 𝑦 ∧ 𝑦 < 𝑤 ) )
33	25 32	r19.29a	⊢ ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) → ( ( 𝑧 (,) 𝑤 ) ∩ ℚ ) ≠ ∅ )
34	33	a1i	⊢ ( 𝑦 = ( 𝑧 (,) 𝑤 ) → ( 𝑥 ∈ ( 𝑧 (,) 𝑤 ) → ( ( 𝑧 (,) 𝑤 ) ∩ ℚ ) ≠ ∅ ) )
35		eleq2	⊢ ( 𝑦 = ( 𝑧 (,) 𝑤 ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ( 𝑧 (,) 𝑤 ) ) )
36		ineq1	⊢ ( 𝑦 = ( 𝑧 (,) 𝑤 ) → ( 𝑦 ∩ ℚ ) = ( ( 𝑧 (,) 𝑤 ) ∩ ℚ ) )
37	36	neeq1d	⊢ ( 𝑦 = ( 𝑧 (,) 𝑤 ) → ( ( 𝑦 ∩ ℚ ) ≠ ∅ ↔ ( ( 𝑧 (,) 𝑤 ) ∩ ℚ ) ≠ ∅ ) )
38	34 35 37	3imtr4d	⊢ ( 𝑦 = ( 𝑧 (,) 𝑤 ) → ( 𝑥 ∈ 𝑦 → ( 𝑦 ∩ ℚ ) ≠ ∅ ) )
39	38	rexlimivw	⊢ ( ∃ 𝑤 ∈ ℝ* 𝑦 = ( 𝑧 (,) 𝑤 ) → ( 𝑥 ∈ 𝑦 → ( 𝑦 ∩ ℚ ) ≠ ∅ ) )
40	39	rexlimivw	⊢ ( ∃ 𝑧 ∈ ℝ* ∃ 𝑤 ∈ ℝ* 𝑦 = ( 𝑧 (,) 𝑤 ) → ( 𝑥 ∈ 𝑦 → ( 𝑦 ∩ ℚ ) ≠ ∅ ) )
41	9 40	sylbi	⊢ ( 𝑦 ∈ ran (,) → ( 𝑥 ∈ 𝑦 → ( 𝑦 ∩ ℚ ) ≠ ∅ ) )
42	41	rgen	⊢ ∀ 𝑦 ∈ ran (,) ( 𝑥 ∈ 𝑦 → ( 𝑦 ∩ ℚ ) ≠ ∅ )
43		eqidd	⊢ ( 𝑥 ∈ ℝ → ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) ) )
44	3	a1i	⊢ ( 𝑥 ∈ ℝ → ℝ = ∪ ( topGen ‘ ran (,) ) )
45		retopbas	⊢ ran (,) ∈ TopBases
46	45	a1i	⊢ ( 𝑥 ∈ ℝ → ran (,) ∈ TopBases )
47	2	a1i	⊢ ( 𝑥 ∈ ℝ → ℚ ⊆ ℝ )
48		id	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ )
49	43 44 46 47 48	elcls3	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) ↔ ∀ 𝑦 ∈ ran (,) ( 𝑥 ∈ 𝑦 → ( 𝑦 ∩ ℚ ) ≠ ∅ ) ) )
50	42 49	mpbiri	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) )
51	50	ssriv	⊢ ℝ ⊆ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ )
52	5 51	eqssi	⊢ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) = ℝ