This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iocpnfordt

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 iocpnfordt 
|- ( A (,] +oo ) 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 ssun1 
 |-  ran ( x e. RR* |-> ( x (,] +oo ) ) C_ ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) )
14 eqid 
 |-  ( A (,] +oo ) = ( A (,] +oo )
15 oveq1 
 |-  ( x = A -> ( x (,] +oo ) = ( A (,] +oo ) )
16 15 rspceeqv 
 |-  ( ( A e. RR* /\ ( A (,] +oo ) = ( A (,] +oo ) ) -> E. x e. RR* ( A (,] +oo ) = ( x (,] +oo ) )
17 14 16 mpan2 
 |-  ( A e. RR* -> E. x e. RR* ( A (,] +oo ) = ( x (,] +oo ) )
18 eqid 
 |-  ( x e. RR* |-> ( x (,] +oo ) ) = ( x e. RR* |-> ( x (,] +oo ) )
19 ovex 
 |-  ( x (,] +oo ) e. _V
20 18 19 elrnmpti 
 |-  ( ( A (,] +oo ) e. ran ( x e. RR* |-> ( x (,] +oo ) ) <-> E. x e. RR* ( A (,] +oo ) = ( x (,] +oo ) )
21 17 20 sylibr 
 |-  ( A e. RR* -> ( A (,] +oo ) e. ran ( x e. RR* |-> ( x (,] +oo ) ) )
22 13 21 sselid 
 |-  ( A e. RR* -> ( A (,] +oo ) e. ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) )
23 12 22 sselid 
 |-  ( A e. RR* -> ( A (,] +oo ) e. ( ( ran ( x e. RR* |-> ( x (,] +oo ) ) u. ran ( x e. RR* |-> ( -oo [,) x ) ) ) u. ran (,) ) )
24 11 23 sselid 
 |-  ( A e. RR* -> ( A (,] +oo ) e. ( ordTop ` <_ ) )
25 24 adantr 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( A (,] +oo ) e. ( ordTop ` <_ ) )
26 df-ioc 
 |-  (,] = ( 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 
 |-  ( -. ( A e. RR* /\ +oo e. RR* ) -> ( A (,] +oo ) = (/) )
30 0opn 
 |-  ( ( ordTop ` <_ ) e. Top -> (/) e. ( ordTop ` <_ ) )
31 5 30 ax-mp 
 |-  (/) e. ( ordTop ` <_ )
32 29 31 eqeltrdi 
 |-  ( -. ( A e. RR* /\ +oo e. RR* ) -> ( A (,] +oo ) e. ( ordTop ` <_ ) )
33 25 32 pm2.61i 
 |-  ( A (,] +oo ) e. ( ordTop ` <_ )