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

Metamath Proof Explorer

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 (,) ) ) ‘ ℚ ) = ℝ