Step |
Hyp |
Ref |
Expression |
1 |
|
neg1rr |
|- -u 1 e. RR |
2 |
|
1re |
|- 1 e. RR |
3 |
|
neg1lt0 |
|- -u 1 < 0 |
4 |
|
0lt1 |
|- 0 < 1 |
5 |
|
0re |
|- 0 e. RR |
6 |
1 5 2
|
lttri |
|- ( ( -u 1 < 0 /\ 0 < 1 ) -> -u 1 < 1 ) |
7 |
3 4 6
|
mp2an |
|- -u 1 < 1 |
8 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
9 |
|
eqid |
|- ( x e. ( 0 [,] 1 ) |-> ( ( x x. 1 ) + ( ( 1 - x ) x. -u 1 ) ) ) = ( x e. ( 0 [,] 1 ) |-> ( ( x x. 1 ) + ( ( 1 - x ) x. -u 1 ) ) ) |
10 |
8 9
|
icchmeo |
|- ( ( -u 1 e. RR /\ 1 e. RR /\ -u 1 < 1 ) -> ( x e. ( 0 [,] 1 ) |-> ( ( x x. 1 ) + ( ( 1 - x ) x. -u 1 ) ) ) e. ( II Homeo ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) ) ) |
11 |
1 2 7 10
|
mp3an |
|- ( x e. ( 0 [,] 1 ) |-> ( ( x x. 1 ) + ( ( 1 - x ) x. -u 1 ) ) ) e. ( II Homeo ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) ) |
12 |
|
hmphi |
|- ( ( x e. ( 0 [,] 1 ) |-> ( ( x x. 1 ) + ( ( 1 - x ) x. -u 1 ) ) ) e. ( II Homeo ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) ) -> II ~= ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) ) |
13 |
11 12
|
ax-mp |
|- II ~= ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) |
14 |
|
eqid |
|- ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) |
15 |
|
eqid |
|- ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` y ) , -e ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` -u y ) ) ) = ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` y ) , -e ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` -u y ) ) ) |
16 |
14 15 8
|
xrhmeo |
|- ( ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` y ) , -e ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` -u y ) ) ) Isom < , < ( ( -u 1 [,] 1 ) , RR* ) /\ ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` y ) , -e ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` -u y ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) Homeo ( ordTop ` <_ ) ) ) |
17 |
16
|
simpri |
|- ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` y ) , -e ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` -u y ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) Homeo ( ordTop ` <_ ) ) |
18 |
|
hmphi |
|- ( ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` y ) , -e ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` -u y ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) Homeo ( ordTop ` <_ ) ) -> ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) ~= ( ordTop ` <_ ) ) |
19 |
17 18
|
ax-mp |
|- ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) ~= ( ordTop ` <_ ) |
20 |
|
hmphtr |
|- ( ( II ~= ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) /\ ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) ~= ( ordTop ` <_ ) ) -> II ~= ( ordTop ` <_ ) ) |
21 |
13 19 20
|
mp2an |
|- II ~= ( ordTop ` <_ ) |