Metamath Proof Explorer

Theorem tgqioo

Description: The topology generated by open intervals of reals with rational endpoints is the same as the open sets of the standard metric space on the reals. In particular, this proves that the standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Hypothesis tgqioo.1 
|- Q = ( topGen ` ( (,) " ( QQ X. QQ ) ) )
Assertion tgqioo 
|- ( topGen ` ran (,) ) = Q

Proof

Step Hyp Ref Expression
1 tgqioo.1 
 |-  Q = ( topGen ` ( (,) " ( QQ X. QQ ) ) )
2 imassrn 
 |-  ( (,) " ( QQ X. QQ ) ) C_ ran (,)
3 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
4 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
5 3 4 ax-mp 
 |-  (,) Fn ( RR* X. RR* )
6 simpll 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) -> x e. RR* )
7 elioo1 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( z e. ( x (,) y ) <-> ( z e. RR* /\ x < z /\ z < y ) ) )
8 7 biimpa 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) -> ( z e. RR* /\ x < z /\ z < y ) )
9 8 simp1d 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) -> z e. RR* )
10 8 simp2d 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) -> x < z )
11 qbtwnxr 
 |-  ( ( x e. RR* /\ z e. RR* /\ x < z ) -> E. u e. QQ ( x < u /\ u < z ) )
12 6 9 10 11 syl3anc 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) -> E. u e. QQ ( x < u /\ u < z ) )
13 simplr 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) -> y e. RR* )
14 8 simp3d 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) -> z < y )
15 qbtwnxr 
 |-  ( ( z e. RR* /\ y e. RR* /\ z < y ) -> E. v e. QQ ( z < v /\ v < y ) )
16 9 13 14 15 syl3anc 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) -> E. v e. QQ ( z < v /\ v < y ) )
17 reeanv 
 |-  ( E. u e. QQ E. v e. QQ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) <-> ( E. u e. QQ ( x < u /\ u < z ) /\ E. v e. QQ ( z < v /\ v < y ) ) )
18 df-ov 
 |-  ( u (,) v ) = ( (,) ` <. u , v >. )
19 opelxpi 
 |-  ( ( u e. QQ /\ v e. QQ ) -> <. u , v >. e. ( QQ X. QQ ) )
20 19 3ad2ant2 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> <. u , v >. e. ( QQ X. QQ ) )
21 ffun 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> Fun (,) )
22 3 21 ax-mp 
 |-  Fun (,)
23 qssre 
 |-  QQ C_ RR
24 ressxr 
 |-  RR C_ RR*
25 23 24 sstri 
 |-  QQ C_ RR*
26 xpss12 
 |-  ( ( QQ C_ RR* /\ QQ C_ RR* ) -> ( QQ X. QQ ) C_ ( RR* X. RR* ) )
27 25 25 26 mp2an 
 |-  ( QQ X. QQ ) C_ ( RR* X. RR* )
28 3 fdmi 
 |-  dom (,) = ( RR* X. RR* )
29 27 28 sseqtrri 
 |-  ( QQ X. QQ ) C_ dom (,)
30 funfvima2 
 |-  ( ( Fun (,) /\ ( QQ X. QQ ) C_ dom (,) ) -> ( <. u , v >. e. ( QQ X. QQ ) -> ( (,) ` <. u , v >. ) e. ( (,) " ( QQ X. QQ ) ) ) )
31 22 29 30 mp2an 
 |-  ( <. u , v >. e. ( QQ X. QQ ) -> ( (,) ` <. u , v >. ) e. ( (,) " ( QQ X. QQ ) ) )
32 20 31 syl 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> ( (,) ` <. u , v >. ) e. ( (,) " ( QQ X. QQ ) ) )
33 18 32 eqeltrid 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> ( u (,) v ) e. ( (,) " ( QQ X. QQ ) ) )
34 9 3ad2ant1 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> z e. RR* )
35 simp3lr 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> u < z )
36 simp3rl 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> z < v )
37 simp2l 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> u e. QQ )
38 25 37 sselid 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> u e. RR* )
39 simp2r 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> v e. QQ )
40 25 39 sselid 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> v e. RR* )
41 elioo1 
 |-  ( ( u e. RR* /\ v e. RR* ) -> ( z e. ( u (,) v ) <-> ( z e. RR* /\ u < z /\ z < v ) ) )
42 38 40 41 syl2anc 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> ( z e. ( u (,) v ) <-> ( z e. RR* /\ u < z /\ z < v ) ) )
43 34 35 36 42 mpbir3and 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> z e. ( u (,) v ) )
44 6 3ad2ant1 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> x e. RR* )
45 simp3ll 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> x < u )
46 44 38 45 xrltled 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> x <_ u )
47 iooss1 
 |-  ( ( x e. RR* /\ x <_ u ) -> ( u (,) v ) C_ ( x (,) v ) )
48 44 46 47 syl2anc 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> ( u (,) v ) C_ ( x (,) v ) )
49 13 3ad2ant1 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> y e. RR* )
50 simp3rr 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> v < y )
51 40 49 50 xrltled 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> v <_ y )
52 iooss2 
 |-  ( ( y e. RR* /\ v <_ y ) -> ( x (,) v ) C_ ( x (,) y ) )
53 49 51 52 syl2anc 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> ( x (,) v ) C_ ( x (,) y ) )
54 48 53 sstrd 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> ( u (,) v ) C_ ( x (,) y ) )
55 eleq2 
 |-  ( w = ( u (,) v ) -> ( z e. w <-> z e. ( u (,) v ) ) )
56 sseq1 
 |-  ( w = ( u (,) v ) -> ( w C_ ( x (,) y ) <-> ( u (,) v ) C_ ( x (,) y ) ) )
57 55 56 anbi12d 
 |-  ( w = ( u (,) v ) -> ( ( z e. w /\ w C_ ( x (,) y ) ) <-> ( z e. ( u (,) v ) /\ ( u (,) v ) C_ ( x (,) y ) ) ) )
58 57 rspcev 
 |-  ( ( ( u (,) v ) e. ( (,) " ( QQ X. QQ ) ) /\ ( z e. ( u (,) v ) /\ ( u (,) v ) C_ ( x (,) y ) ) ) -> E. w e. ( (,) " ( QQ X. QQ ) ) ( z e. w /\ w C_ ( x (,) y ) ) )
59 33 43 54 58 syl12anc 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) /\ ( u e. QQ /\ v e. QQ ) /\ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) ) -> E. w e. ( (,) " ( QQ X. QQ ) ) ( z e. w /\ w C_ ( x (,) y ) ) )
60 59 3exp 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) -> ( ( u e. QQ /\ v e. QQ ) -> ( ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) -> E. w e. ( (,) " ( QQ X. QQ ) ) ( z e. w /\ w C_ ( x (,) y ) ) ) ) )
61 60 rexlimdvv 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) -> ( E. u e. QQ E. v e. QQ ( ( x < u /\ u < z ) /\ ( z < v /\ v < y ) ) -> E. w e. ( (,) " ( QQ X. QQ ) ) ( z e. w /\ w C_ ( x (,) y ) ) ) )
62 17 61 biimtrrid 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) -> ( ( E. u e. QQ ( x < u /\ u < z ) /\ E. v e. QQ ( z < v /\ v < y ) ) -> E. w e. ( (,) " ( QQ X. QQ ) ) ( z e. w /\ w C_ ( x (,) y ) ) ) )
63 12 16 62 mp2and 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ z e. ( x (,) y ) ) -> E. w e. ( (,) " ( QQ X. QQ ) ) ( z e. w /\ w C_ ( x (,) y ) ) )
64 63 ralrimiva 
 |-  ( ( x e. RR* /\ y e. RR* ) -> A. z e. ( x (,) y ) E. w e. ( (,) " ( QQ X. QQ ) ) ( z e. w /\ w C_ ( x (,) y ) ) )
65 qtopbas 
 |-  ( (,) " ( QQ X. QQ ) ) e. TopBases
66 eltg2b 
 |-  ( ( (,) " ( QQ X. QQ ) ) e. TopBases -> ( ( x (,) y ) e. ( topGen ` ( (,) " ( QQ X. QQ ) ) ) <-> A. z e. ( x (,) y ) E. w e. ( (,) " ( QQ X. QQ ) ) ( z e. w /\ w C_ ( x (,) y ) ) ) )
67 65 66 ax-mp 
 |-  ( ( x (,) y ) e. ( topGen ` ( (,) " ( QQ X. QQ ) ) ) <-> A. z e. ( x (,) y ) E. w e. ( (,) " ( QQ X. QQ ) ) ( z e. w /\ w C_ ( x (,) y ) ) )
68 64 67 sylibr 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x (,) y ) e. ( topGen ` ( (,) " ( QQ X. QQ ) ) ) )
69 68 rgen2 
 |-  A. x e. RR* A. y e. RR* ( x (,) y ) e. ( topGen ` ( (,) " ( QQ X. QQ ) ) )
70 ffnov 
 |-  ( (,) : ( RR* X. RR* ) --> ( topGen ` ( (,) " ( QQ X. QQ ) ) ) <-> ( (,) Fn ( RR* X. RR* ) /\ A. x e. RR* A. y e. RR* ( x (,) y ) e. ( topGen ` ( (,) " ( QQ X. QQ ) ) ) ) )
71 5 69 70 mpbir2an 
 |-  (,) : ( RR* X. RR* ) --> ( topGen ` ( (,) " ( QQ X. QQ ) ) )
72 frn 
 |-  ( (,) : ( RR* X. RR* ) --> ( topGen ` ( (,) " ( QQ X. QQ ) ) ) -> ran (,) C_ ( topGen ` ( (,) " ( QQ X. QQ ) ) ) )
73 71 72 ax-mp 
 |-  ran (,) C_ ( topGen ` ( (,) " ( QQ X. QQ ) ) )
74 2basgen 
 |-  ( ( ( (,) " ( QQ X. QQ ) ) C_ ran (,) /\ ran (,) C_ ( topGen ` ( (,) " ( QQ X. QQ ) ) ) ) -> ( topGen ` ( (,) " ( QQ X. QQ ) ) ) = ( topGen ` ran (,) ) )
75 2 73 74 mp2an 
 |-  ( topGen ` ( (,) " ( QQ X. QQ ) ) ) = ( topGen ` ran (,) )
76 1 75 eqtr2i 
 |-  ( topGen ` ran (,) ) = Q