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