Metamath Proof Explorer

Theorem icomnfordt

Description: An unbounded above open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion icomnfordt 
|- ( -oo [,) A ) e. ( ordTop ` <_ )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ran ( x e. RR* |-> ( x (,] +oo ) ) = ran ( x e. RR* |-> ( x (,] +oo ) )
2 eqid 
 |-  ran ( x e. RR* |-> ( -oo [,) x ) ) = ran ( x e. RR* |-> ( -oo [,) x ) )
3 eqid 
 |-  ran (,) = ran (,)
4 1 2 3 leordtval 
 |-  ( ordTop ` <_ ) = ( topGen ` ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) ) )
5 letop 
 |-  ( ordTop ` <_ ) e. Top
6 4 5 eqeltrri 
 |-  ( topGen ` ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) ) ) e. Top
7 tgclb 
 |-  ( ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) ) e. TopBases <-> ( topGen ` ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) ) ) e. Top )
8 6 7 mpbir 
 |-  ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) ) e. TopBases
9 bastg 
 |-  ( ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) ) e. TopBases -> ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) ) C_ ( topGen ` ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) ) ) )
10 8 9 ax-mp 
 |-  ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) ) C_ ( topGen ` ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) ) )
11 10 4 sseqtrri 
 |-  ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) ) C_ ( ordTop ` <_ )
12 ssun1 
 |-  ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) C_ ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) )
13 ssun2 
 |-  ran ( x e. RR* |-> ( -oo [,) x ) ) C_ ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) )
14 eqid 
 |-  ( -oo [,) A ) = ( -oo [,) A )
15 oveq2 
 |-  ( x = A -> ( -oo [,) x ) = ( -oo [,) A ) )
16 15 rspceeqv 
 |-  ( ( A e. RR* /\ ( -oo [,) A ) = ( -oo [,) A ) ) -> E. x e. RR* ( -oo [,) A ) = ( -oo [,) x ) )
17 14 16 mpan2 
 |-  ( A e. RR* -> E. x e. RR* ( -oo [,) A ) = ( -oo [,) x ) )
18 eqid 
 |-  ( x e. RR* |-> ( -oo [,) x ) ) = ( x e. RR* |-> ( -oo [,) x ) )
19 ovex 
 |-  ( -oo [,) x ) e. _V
20 18 19 elrnmpti 
 |-  ( ( -oo [,) A ) e. ran ( x e. RR* |-> ( -oo [,) x ) ) <-> E. x e. RR* ( -oo [,) A ) = ( -oo [,) x ) )
21 17 20 sylibr 
 |-  ( A e. RR* -> ( -oo [,) A ) e. ran ( x e. RR* |-> ( -oo [,) x ) ) )
22 13 21 sselid 
 |-  ( A e. RR* -> ( -oo [,) A ) e. ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) )
23 12 22 sselid 
 |-  ( A e. RR* -> ( -oo [,) A ) e. ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) ) )
24 11 23 sselid 
 |-  ( A e. RR* -> ( -oo [,) A ) e. ( ordTop ` <_ ) )
25 24 adantl 
 |-  ( ( -oo e. RR* /\ A e. RR* ) -> ( -oo [,) A ) e. ( ordTop ` <_ ) )
26 df-ico 
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
27 26 ixxf 
 |-  [,) : ( RR* X. RR* ) --> ~P RR*
28 27 fdmi 
 |-  dom [,) = ( RR* X. RR* )
29 28 ndmov 
 |-  ( -. ( -oo e. RR* /\ A e. RR* ) -> ( -oo [,) A ) = (/) )
30 0opn 
 |-  ( ( ordTop ` <_ ) e. Top -> (/) e. ( ordTop ` <_ ) )
31 5 30 ax-mp 
 |-  (/) e. ( ordTop ` <_ )
32 29 31 eqeltrdi 
 |-  ( -. ( -oo e. RR* /\ A e. RR* ) -> ( -oo [,) A ) e. ( ordTop ` <_ ) )
33 25 32 pm2.61i 
 |-  ( -oo [,) A ) e. ( ordTop ` <_ )