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 ` <_ ) |