Metamath Proof Explorer

Theorem lecldbas

Description: The set of closed intervals forms a closed subbasis for the topology on the extended reals. Since our definition of a basis is in terms of open sets, we express this by showing that the complements of closed intervals form an open subbasis for the topology. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis lecldbas.1 
|- F = ( x e. ran [,] |-> ( RR* \ x ) )
Assertion lecldbas 
|- ( ordTop ` <_ ) = ( topGen ` ( fi ` ran F ) )

Proof

Step Hyp Ref Expression
1 lecldbas.1 
 |-  F = ( x e. ran [,] |-> ( RR* \ x ) )
2 eqid 
 |-  ran ( y e. RR* |-> ( y (,] +oo ) ) = ran ( y e. RR* |-> ( y (,] +oo ) )
3 eqid 
 |-  ran ( y e. RR* |-> ( -oo [,) y ) ) = ran ( y e. RR* |-> ( -oo [,) y ) )
4 2 3 leordtval2 
 |-  ( ordTop ` <_ ) = ( topGen ` ( fi ` ( ran ( y e. RR* |-> ( y (,] +oo ) ) u. ran ( y e. RR* |-> ( -oo [,) y ) ) ) ) )
5 fvex 
 |-  ( fi ` ran F ) e. _V
6 fvex 
 |-  ( ordTop ` <_ ) e. _V
7 iccf 
 |-  [,] : ( RR* X. RR* ) --> ~P RR*
8 ffn 
 |-  ( [,] : ( RR* X. RR* ) --> ~P RR* -> [,] Fn ( RR* X. RR* ) )
9 7 8 ax-mp 
 |-  [,] Fn ( RR* X. RR* )
10 ovelrn 
 |-  ( [,] Fn ( RR* X. RR* ) -> ( x e. ran [,] <-> E. a e. RR* E. b e. RR* x = ( a [,] b ) ) )
11 9 10 ax-mp 
 |-  ( x e. ran [,] <-> E. a e. RR* E. b e. RR* x = ( a [,] b ) )
12 difeq2 
 |-  ( x = ( a [,] b ) -> ( RR* \ x ) = ( RR* \ ( a [,] b ) ) )
13 iccordt 
 |-  ( a [,] b ) e. ( Clsd ` ( ordTop ` <_ ) )
14 letopuni 
 |-  RR* = U. ( ordTop ` <_ )
15 14 cldopn 
 |-  ( ( a [,] b ) e. ( Clsd ` ( ordTop ` <_ ) ) -> ( RR* \ ( a [,] b ) ) e. ( ordTop ` <_ ) )
16 13 15 ax-mp 
 |-  ( RR* \ ( a [,] b ) ) e. ( ordTop ` <_ )
17 12 16 eqeltrdi 
 |-  ( x = ( a [,] b ) -> ( RR* \ x ) e. ( ordTop ` <_ ) )
18 17 rexlimivw 
 |-  ( E. b e. RR* x = ( a [,] b ) -> ( RR* \ x ) e. ( ordTop ` <_ ) )
19 18 rexlimivw 
 |-  ( E. a e. RR* E. b e. RR* x = ( a [,] b ) -> ( RR* \ x ) e. ( ordTop ` <_ ) )
20 11 19 sylbi 
 |-  ( x e. ran [,] -> ( RR* \ x ) e. ( ordTop ` <_ ) )
21 1 20 fmpti 
 |-  F : ran [,] --> ( ordTop ` <_ )
22 frn 
 |-  ( F : ran [,] --> ( ordTop ` <_ ) -> ran F C_ ( ordTop ` <_ ) )
23 21 22 ax-mp 
 |-  ran F C_ ( ordTop ` <_ )
24 6 23 ssexi 
 |-  ran F e. _V
25 eqid 
 |-  ( y e. RR* |-> ( y (,] +oo ) ) = ( y e. RR* |-> ( y (,] +oo ) )
26 mnfxr 
 |-  -oo e. RR*
27 fnovrn 
 |-  ( ( [,] Fn ( RR* X. RR* ) /\ -oo e. RR* /\ y e. RR* ) -> ( -oo [,] y ) e. ran [,] )
28 9 26 27 mp3an12 
 |-  ( y e. RR* -> ( -oo [,] y ) e. ran [,] )
29 26 a1i 
 |-  ( y e. RR* -> -oo e. RR* )
30 id 
 |-  ( y e. RR* -> y e. RR* )
31 pnfxr 
 |-  +oo e. RR*
32 31 a1i 
 |-  ( y e. RR* -> +oo e. RR* )
33 mnfle 
 |-  ( y e. RR* -> -oo <_ y )
34 pnfge 
 |-  ( y e. RR* -> y <_ +oo )
35 df-icc 
 |-  [,] = ( a e. RR* , b e. RR* |-> { c e. RR* | ( a <_ c /\ c <_ b ) } )
36 df-ioc 
 |-  (,] = ( a e. RR* , b e. RR* |-> { c e. RR* | ( a < c /\ c <_ b ) } )
37 xrltnle 
 |-  ( ( y e. RR* /\ z e. RR* ) -> ( y < z <-> -. z <_ y ) )
38 xrletr 
 |-  ( ( z e. RR* /\ y e. RR* /\ +oo e. RR* ) -> ( ( z <_ y /\ y <_ +oo ) -> z <_ +oo ) )
39 xrlelttr 
 |-  ( ( -oo e. RR* /\ y e. RR* /\ z e. RR* ) -> ( ( -oo <_ y /\ y < z ) -> -oo < z ) )
40 xrltle 
 |-  ( ( -oo e. RR* /\ z e. RR* ) -> ( -oo < z -> -oo <_ z ) )
41 40 3adant2 
 |-  ( ( -oo e. RR* /\ y e. RR* /\ z e. RR* ) -> ( -oo < z -> -oo <_ z ) )
42 39 41 syld 
 |-  ( ( -oo e. RR* /\ y e. RR* /\ z e. RR* ) -> ( ( -oo <_ y /\ y < z ) -> -oo <_ z ) )
43 35 36 37 35 38 42 ixxun 
 |-  ( ( ( -oo e. RR* /\ y e. RR* /\ +oo e. RR* ) /\ ( -oo <_ y /\ y <_ +oo ) ) -> ( ( -oo [,] y ) u. ( y (,] +oo ) ) = ( -oo [,] +oo ) )
44 29 30 32 33 34 43 syl32anc 
 |-  ( y e. RR* -> ( ( -oo [,] y ) u. ( y (,] +oo ) ) = ( -oo [,] +oo ) )
45 iccmax 
 |-  ( -oo [,] +oo ) = RR*
46 44 45 eqtrdi 
 |-  ( y e. RR* -> ( ( -oo [,] y ) u. ( y (,] +oo ) ) = RR* )
47 iccssxr 
 |-  ( -oo [,] y ) C_ RR*
48 35 36 37 ixxdisj 
 |-  ( ( -oo e. RR* /\ y e. RR* /\ +oo e. RR* ) -> ( ( -oo [,] y ) i^i ( y (,] +oo ) ) = (/) )
49 26 31 48 mp3an13 
 |-  ( y e. RR* -> ( ( -oo [,] y ) i^i ( y (,] +oo ) ) = (/) )
50 uneqdifeq 
 |-  ( ( ( -oo [,] y ) C_ RR* /\ ( ( -oo [,] y ) i^i ( y (,] +oo ) ) = (/) ) -> ( ( ( -oo [,] y ) u. ( y (,] +oo ) ) = RR* <-> ( RR* \ ( -oo [,] y ) ) = ( y (,] +oo ) ) )
51 47 49 50 sylancr 
 |-  ( y e. RR* -> ( ( ( -oo [,] y ) u. ( y (,] +oo ) ) = RR* <-> ( RR* \ ( -oo [,] y ) ) = ( y (,] +oo ) ) )
52 46 51 mpbid 
 |-  ( y e. RR* -> ( RR* \ ( -oo [,] y ) ) = ( y (,] +oo ) )
53 52 eqcomd 
 |-  ( y e. RR* -> ( y (,] +oo ) = ( RR* \ ( -oo [,] y ) ) )
54 difeq2 
 |-  ( x = ( -oo [,] y ) -> ( RR* \ x ) = ( RR* \ ( -oo [,] y ) ) )
55 54 rspceeqv 
 |-  ( ( ( -oo [,] y ) e. ran [,] /\ ( y (,] +oo ) = ( RR* \ ( -oo [,] y ) ) ) -> E. x e. ran [,] ( y (,] +oo ) = ( RR* \ x ) )
56 28 53 55 syl2anc 
 |-  ( y e. RR* -> E. x e. ran [,] ( y (,] +oo ) = ( RR* \ x ) )
57 xrex 
 |-  RR* e. _V
58 57 difexi 
 |-  ( RR* \ x ) e. _V
59 1 58 elrnmpti 
 |-  ( ( y (,] +oo ) e. ran F <-> E. x e. ran [,] ( y (,] +oo ) = ( RR* \ x ) )
60 56 59 sylibr 
 |-  ( y e. RR* -> ( y (,] +oo ) e. ran F )
61 25 60 fmpti 
 |-  ( y e. RR* |-> ( y (,] +oo ) ) : RR* --> ran F
62 frn 
 |-  ( ( y e. RR* |-> ( y (,] +oo ) ) : RR* --> ran F -> ran ( y e. RR* |-> ( y (,] +oo ) ) C_ ran F )
63 61 62 ax-mp 
 |-  ran ( y e. RR* |-> ( y (,] +oo ) ) C_ ran F
64 eqid 
 |-  ( y e. RR* |-> ( -oo [,) y ) ) = ( y e. RR* |-> ( -oo [,) y ) )
65 fnovrn 
 |-  ( ( [,] Fn ( RR* X. RR* ) /\ y e. RR* /\ +oo e. RR* ) -> ( y [,] +oo ) e. ran [,] )
66 9 31 65 mp3an13 
 |-  ( y e. RR* -> ( y [,] +oo ) e. ran [,] )
67 df-ico 
 |-  [,) = ( a e. RR* , b e. RR* |-> { c e. RR* | ( a <_ c /\ c < b ) } )
68 xrlenlt 
 |-  ( ( y e. RR* /\ z e. RR* ) -> ( y <_ z <-> -. z < y ) )
69 xrltletr 
 |-  ( ( z e. RR* /\ y e. RR* /\ +oo e. RR* ) -> ( ( z < y /\ y <_ +oo ) -> z < +oo ) )
70 xrltle 
 |-  ( ( z e. RR* /\ +oo e. RR* ) -> ( z < +oo -> z <_ +oo ) )
71 70 3adant2 
 |-  ( ( z e. RR* /\ y e. RR* /\ +oo e. RR* ) -> ( z < +oo -> z <_ +oo ) )
72 69 71 syld 
 |-  ( ( z e. RR* /\ y e. RR* /\ +oo e. RR* ) -> ( ( z < y /\ y <_ +oo ) -> z <_ +oo ) )
73 xrletr 
 |-  ( ( -oo e. RR* /\ y e. RR* /\ z e. RR* ) -> ( ( -oo <_ y /\ y <_ z ) -> -oo <_ z ) )
74 67 35 68 35 72 73 ixxun 
 |-  ( ( ( -oo e. RR* /\ y e. RR* /\ +oo e. RR* ) /\ ( -oo <_ y /\ y <_ +oo ) ) -> ( ( -oo [,) y ) u. ( y [,] +oo ) ) = ( -oo [,] +oo ) )
75 29 30 32 33 34 74 syl32anc 
 |-  ( y e. RR* -> ( ( -oo [,) y ) u. ( y [,] +oo ) ) = ( -oo [,] +oo ) )
76 uncom 
 |-  ( ( -oo [,) y ) u. ( y [,] +oo ) ) = ( ( y [,] +oo ) u. ( -oo [,) y ) )
77 75 76 45 3eqtr3g 
 |-  ( y e. RR* -> ( ( y [,] +oo ) u. ( -oo [,) y ) ) = RR* )
78 iccssxr 
 |-  ( y [,] +oo ) C_ RR*
79 incom 
 |-  ( ( y [,] +oo ) i^i ( -oo [,) y ) ) = ( ( -oo [,) y ) i^i ( y [,] +oo ) )
80 67 35 68 ixxdisj 
 |-  ( ( -oo e. RR* /\ y e. RR* /\ +oo e. RR* ) -> ( ( -oo [,) y ) i^i ( y [,] +oo ) ) = (/) )
81 26 31 80 mp3an13 
 |-  ( y e. RR* -> ( ( -oo [,) y ) i^i ( y [,] +oo ) ) = (/) )
82 79 81 syl5eq 
 |-  ( y e. RR* -> ( ( y [,] +oo ) i^i ( -oo [,) y ) ) = (/) )
83 uneqdifeq 
 |-  ( ( ( y [,] +oo ) C_ RR* /\ ( ( y [,] +oo ) i^i ( -oo [,) y ) ) = (/) ) -> ( ( ( y [,] +oo ) u. ( -oo [,) y ) ) = RR* <-> ( RR* \ ( y [,] +oo ) ) = ( -oo [,) y ) ) )
84 78 82 83 sylancr 
 |-  ( y e. RR* -> ( ( ( y [,] +oo ) u. ( -oo [,) y ) ) = RR* <-> ( RR* \ ( y [,] +oo ) ) = ( -oo [,) y ) ) )
85 77 84 mpbid 
 |-  ( y e. RR* -> ( RR* \ ( y [,] +oo ) ) = ( -oo [,) y ) )
86 85 eqcomd 
 |-  ( y e. RR* -> ( -oo [,) y ) = ( RR* \ ( y [,] +oo ) ) )
87 difeq2 
 |-  ( x = ( y [,] +oo ) -> ( RR* \ x ) = ( RR* \ ( y [,] +oo ) ) )
88 87 rspceeqv 
 |-  ( ( ( y [,] +oo ) e. ran [,] /\ ( -oo [,) y ) = ( RR* \ ( y [,] +oo ) ) ) -> E. x e. ran [,] ( -oo [,) y ) = ( RR* \ x ) )
89 66 86 88 syl2anc 
 |-  ( y e. RR* -> E. x e. ran [,] ( -oo [,) y ) = ( RR* \ x ) )
90 1 58 elrnmpti 
 |-  ( ( -oo [,) y ) e. ran F <-> E. x e. ran [,] ( -oo [,) y ) = ( RR* \ x ) )
91 89 90 sylibr 
 |-  ( y e. RR* -> ( -oo [,) y ) e. ran F )
92 64 91 fmpti 
 |-  ( y e. RR* |-> ( -oo [,) y ) ) : RR* --> ran F
93 frn 
 |-  ( ( y e. RR* |-> ( -oo [,) y ) ) : RR* --> ran F -> ran ( y e. RR* |-> ( -oo [,) y ) ) C_ ran F )
94 92 93 ax-mp 
 |-  ran ( y e. RR* |-> ( -oo [,) y ) ) C_ ran F
95 63 94 unssi 
 |-  ( ran ( y e. RR* |-> ( y (,] +oo ) ) u. ran ( y e. RR* |-> ( -oo [,) y ) ) ) C_ ran F
96 fiss 
 |-  ( ( ran F e. _V /\ ( ran ( y e. RR* |-> ( y (,] +oo ) ) u. ran ( y e. RR* |-> ( -oo [,) y ) ) ) C_ ran F ) -> ( fi ` ( ran ( y e. RR* |-> ( y (,] +oo ) ) u. ran ( y e. RR* |-> ( -oo [,) y ) ) ) ) C_ ( fi ` ran F ) )
97 24 95 96 mp2an 
 |-  ( fi ` ( ran ( y e. RR* |-> ( y (,] +oo ) ) u. ran ( y e. RR* |-> ( -oo [,) y ) ) ) ) C_ ( fi ` ran F )
98 tgss 
 |-  ( ( ( fi ` ran F ) e. _V /\ ( fi ` ( ran ( y e. RR* |-> ( y (,] +oo ) ) u. ran ( y e. RR* |-> ( -oo [,) y ) ) ) ) C_ ( fi ` ran F ) ) -> ( topGen ` ( fi ` ( ran ( y e. RR* |-> ( y (,] +oo ) ) u. ran ( y e. RR* |-> ( -oo [,) y ) ) ) ) ) C_ ( topGen ` ( fi ` ran F ) ) )
99 5 97 98 mp2an 
 |-  ( topGen ` ( fi ` ( ran ( y e. RR* |-> ( y (,] +oo ) ) u. ran ( y e. RR* |-> ( -oo [,) y ) ) ) ) ) C_ ( topGen ` ( fi ` ran F ) )
100 4 99 eqsstri 
 |-  ( ordTop ` <_ ) C_ ( topGen ` ( fi ` ran F ) )
101 letop 
 |-  ( ordTop ` <_ ) e. Top
102 tgfiss 
 |-  ( ( ( ordTop ` <_ ) e. Top /\ ran F C_ ( ordTop ` <_ ) ) -> ( topGen ` ( fi ` ran F ) ) C_ ( ordTop ` <_ ) )
103 101 23 102 mp2an 
 |-  ( topGen ` ( fi ` ran F ) ) C_ ( ordTop ` <_ )
104 100 103 eqssi 
 |-  ( ordTop ` <_ ) = ( topGen ` ( fi ` ran F ) )