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 (,) ) ) ` QQ ) = RR

Proof

Step Hyp Ref Expression
1 retop
 |-  ( topGen ` ran (,) ) e. Top
2 qssre
 |-  QQ C_ RR
3 uniretop
 |-  RR = U. ( topGen ` ran (,) )
4 3 clsss3
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ QQ C_ RR ) -> ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) C_ RR )
5 1 2 4 mp2an
 |-  ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) C_ RR
6 ioof
 |-  (,) : ( RR* X. RR* ) --> ~P RR
7 ffn
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
8 ovelrn
 |-  ( (,) Fn ( RR* X. RR* ) -> ( y e. ran (,) <-> E. z e. RR* E. w e. RR* y = ( z (,) w ) ) )
9 6 7 8 mp2b
 |-  ( y e. ran (,) <-> E. z e. RR* E. w e. RR* y = ( z (,) w ) )
10 elioo3g
 |-  ( x e. ( z (,) w ) <-> ( ( z e. RR* /\ w e. RR* /\ x e. RR* ) /\ ( z < x /\ x < w ) ) )
11 10 simplbi
 |-  ( x e. ( z (,) w ) -> ( z e. RR* /\ w e. RR* /\ x e. RR* ) )
12 11 simp1d
 |-  ( x e. ( z (,) w ) -> z e. RR* )
13 12 ad2antrr
 |-  ( ( ( x e. ( z (,) w ) /\ y e. QQ ) /\ ( z < y /\ y < w ) ) -> z e. RR* )
14 11 simp2d
 |-  ( x e. ( z (,) w ) -> w e. RR* )
15 14 ad2antrr
 |-  ( ( ( x e. ( z (,) w ) /\ y e. QQ ) /\ ( z < y /\ y < w ) ) -> w e. RR* )
16 qre
 |-  ( y e. QQ -> y e. RR )
17 16 ad2antlr
 |-  ( ( ( x e. ( z (,) w ) /\ y e. QQ ) /\ ( z < y /\ y < w ) ) -> y e. RR )
18 17 rexrd
 |-  ( ( ( x e. ( z (,) w ) /\ y e. QQ ) /\ ( z < y /\ y < w ) ) -> y e. RR* )
19 13 15 18 3jca
 |-  ( ( ( x e. ( z (,) w ) /\ y e. QQ ) /\ ( z < y /\ y < w ) ) -> ( z e. RR* /\ w e. RR* /\ y e. RR* ) )
20 simpr
 |-  ( ( ( x e. ( z (,) w ) /\ y e. QQ ) /\ ( z < y /\ y < w ) ) -> ( z < y /\ y < w ) )
21 elioo3g
 |-  ( y e. ( z (,) w ) <-> ( ( z e. RR* /\ w e. RR* /\ y e. RR* ) /\ ( z < y /\ y < w ) ) )
22 19 20 21 sylanbrc
 |-  ( ( ( x e. ( z (,) w ) /\ y e. QQ ) /\ ( z < y /\ y < w ) ) -> y e. ( z (,) w ) )
23 simplr
 |-  ( ( ( x e. ( z (,) w ) /\ y e. QQ ) /\ ( z < y /\ y < w ) ) -> y e. QQ )
24 inelcm
 |-  ( ( y e. ( z (,) w ) /\ y e. QQ ) -> ( ( z (,) w ) i^i QQ ) =/= (/) )
25 22 23 24 syl2anc
 |-  ( ( ( x e. ( z (,) w ) /\ y e. QQ ) /\ ( z < y /\ y < w ) ) -> ( ( z (,) w ) i^i QQ ) =/= (/) )
26 11 simp3d
 |-  ( x e. ( z (,) w ) -> x e. RR* )
27 eliooord
 |-  ( x e. ( z (,) w ) -> ( z < x /\ x < w ) )
28 27 simpld
 |-  ( x e. ( z (,) w ) -> z < x )
29 27 simprd
 |-  ( x e. ( z (,) w ) -> x < w )
30 12 26 14 28 29 xrlttrd
 |-  ( x e. ( z (,) w ) -> z < w )
31 qbtwnxr
 |-  ( ( z e. RR* /\ w e. RR* /\ z < w ) -> E. y e. QQ ( z < y /\ y < w ) )
32 12 14 30 31 syl3anc
 |-  ( x e. ( z (,) w ) -> E. y e. QQ ( z < y /\ y < w ) )
33 25 32 r19.29a
 |-  ( x e. ( z (,) w ) -> ( ( z (,) w ) i^i QQ ) =/= (/) )
34 33 a1i
 |-  ( y = ( z (,) w ) -> ( x e. ( z (,) w ) -> ( ( z (,) w ) i^i QQ ) =/= (/) ) )
35 eleq2
 |-  ( y = ( z (,) w ) -> ( x e. y <-> x e. ( z (,) w ) ) )
36 ineq1
 |-  ( y = ( z (,) w ) -> ( y i^i QQ ) = ( ( z (,) w ) i^i QQ ) )
37 36 neeq1d
 |-  ( y = ( z (,) w ) -> ( ( y i^i QQ ) =/= (/) <-> ( ( z (,) w ) i^i QQ ) =/= (/) ) )
38 34 35 37 3imtr4d
 |-  ( y = ( z (,) w ) -> ( x e. y -> ( y i^i QQ ) =/= (/) ) )
39 38 rexlimivw
 |-  ( E. w e. RR* y = ( z (,) w ) -> ( x e. y -> ( y i^i QQ ) =/= (/) ) )
40 39 rexlimivw
 |-  ( E. z e. RR* E. w e. RR* y = ( z (,) w ) -> ( x e. y -> ( y i^i QQ ) =/= (/) ) )
41 9 40 sylbi
 |-  ( y e. ran (,) -> ( x e. y -> ( y i^i QQ ) =/= (/) ) )
42 41 rgen
 |-  A. y e. ran (,) ( x e. y -> ( y i^i QQ ) =/= (/) )
43 eqidd
 |-  ( x e. RR -> ( topGen ` ran (,) ) = ( topGen ` ran (,) ) )
44 3 a1i
 |-  ( x e. RR -> RR = U. ( topGen ` ran (,) ) )
45 retopbas
 |-  ran (,) e. TopBases
46 45 a1i
 |-  ( x e. RR -> ran (,) e. TopBases )
47 2 a1i
 |-  ( x e. RR -> QQ C_ RR )
48 id
 |-  ( x e. RR -> x e. RR )
49 43 44 46 47 48 elcls3
 |-  ( x e. RR -> ( x e. ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) <-> A. y e. ran (,) ( x e. y -> ( y i^i QQ ) =/= (/) ) ) )
50 42 49 mpbiri
 |-  ( x e. RR -> x e. ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) )
51 50 ssriv
 |-  RR C_ ( ( cls ` ( topGen ` ran (,) ) ) ` QQ )
52 5 51 eqssi
 |-  ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = RR