Metamath Proof Explorer

Theorem iooordt

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

Ref Expression
Assertion iooordt 
|- ( A (,) B ) 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 ssun2 
 |-  ran (,) C_ ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) )
13 ioorebas 
 |-  ( A (,) B ) e. ran (,)
14 12 13 sselii 
 |-  ( A (,) B ) e. ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) )
15 11 14 sselii 
 |-  ( A (,) B ) e. ( ordTop ` <_ )