Metamath Proof Explorer

Theorem leordtval

Description: The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses leordtval.1 
|- A = ran ( x e. RR* |-> ( x (,] +oo ) )
leordtval.2 
|- B = ran ( x e. RR* |-> ( -oo [,) x ) )
leordtval.3 
|- C = ran (,)
Assertion leordtval 
|- ( ordTop ` <_ ) = ( topGen ` ( ( A u. B ) u. C ) )

Proof

Step Hyp Ref Expression
1 leordtval.1 
 |-  A = ran ( x e. RR* |-> ( x (,] +oo ) )
2 leordtval.2 
 |-  B = ran ( x e. RR* |-> ( -oo [,) x ) )
3 leordtval.3 
 |-  C = ran (,)
4 1 2 leordtval2 
 |-  ( ordTop ` <_ ) = ( topGen ` ( fi ` ( A u. B ) ) )
5 letsr 
 |-  <_ e. TosetRel
6 ledm 
 |-  RR* = dom <_
7 1 leordtvallem1 
 |-  A = ran ( x e. RR* |-> { y e. RR* | -. y <_ x } )
8 1 2 leordtvallem2 
 |-  B = ran ( x e. RR* |-> { y e. RR* | -. x <_ y } )
9 df-ioo 
 |-  (,) = ( a e. RR* , b e. RR* |-> { y e. RR* | ( a < y /\ y < b ) } )
10 xrltnle 
 |-  ( ( a e. RR* /\ y e. RR* ) -> ( a < y <-> -. y <_ a ) )
11 10 adantlr 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ y e. RR* ) -> ( a < y <-> -. y <_ a ) )
12 xrltnle 
 |-  ( ( y e. RR* /\ b e. RR* ) -> ( y < b <-> -. b <_ y ) )
13 12 ancoms 
 |-  ( ( b e. RR* /\ y e. RR* ) -> ( y < b <-> -. b <_ y ) )
14 13 adantll 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ y e. RR* ) -> ( y < b <-> -. b <_ y ) )
15 11 14 anbi12d 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ y e. RR* ) -> ( ( a < y /\ y < b ) <-> ( -. y <_ a /\ -. b <_ y ) ) )
16 15 rabbidva 
 |-  ( ( a e. RR* /\ b e. RR* ) -> { y e. RR* | ( a < y /\ y < b ) } = { y e. RR* | ( -. y <_ a /\ -. b <_ y ) } )
17 16 mpoeq3ia 
 |-  ( a e. RR* , b e. RR* |-> { y e. RR* | ( a < y /\ y < b ) } ) = ( a e. RR* , b e. RR* |-> { y e. RR* | ( -. y <_ a /\ -. b <_ y ) } )
18 9 17 eqtri 
 |-  (,) = ( a e. RR* , b e. RR* |-> { y e. RR* | ( -. y <_ a /\ -. b <_ y ) } )
19 18 rneqi 
 |-  ran (,) = ran ( a e. RR* , b e. RR* |-> { y e. RR* | ( -. y <_ a /\ -. b <_ y ) } )
20 3 19 eqtri 
 |-  C = ran ( a e. RR* , b e. RR* |-> { y e. RR* | ( -. y <_ a /\ -. b <_ y ) } )
21 6 7 8 20 ordtbas2 
 |-  ( <_ e. TosetRel -> ( fi ` ( A u. B ) ) = ( ( A u. B ) u. C ) )
22 5 21 ax-mp 
 |-  ( fi ` ( A u. B ) ) = ( ( A u. B ) u. C )
23 22 fveq2i 
 |-  ( topGen ` ( fi ` ( A u. B ) ) ) = ( topGen ` ( ( A u. B ) u. C ) )
24 4 23 eqtri 
 |-  ( ordTop ` <_ ) = ( topGen ` ( ( A u. B ) u. C ) )