Metamath Proof Explorer

Theorem iirevcn

Description: The reversion function is a continuous map of the unit interval. (Contributed by Mario Carneiro, 6-Jun-2014)

Ref Expression
Assertion iirevcn 
|- ( x e. ( 0 [,] 1 ) |-> ( 1 - x ) ) e. ( II Cn II )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
2 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
3 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
4 3 a1i 
 |-  ( T. -> ( 0 [,] 1 ) C_ RR )
5 iirev 
 |-  ( x e. ( 0 [,] 1 ) -> ( 1 - x ) e. ( 0 [,] 1 ) )
6 5 adantl 
 |-  ( ( T. /\ x e. ( 0 [,] 1 ) ) -> ( 1 - x ) e. ( 0 [,] 1 ) )
7 1 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
8 7 a1i 
 |-  ( T. -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
9 1cnd 
 |-  ( T. -> 1 e. CC )
10 8 8 9 cnmptc 
 |-  ( T. -> ( x e. CC |-> 1 ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
11 8 cnmptid 
 |-  ( T. -> ( x e. CC |-> x ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
12 1 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
13 12 a1i 
 |-  ( T. -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
14 8 10 11 13 cnmpt12f 
 |-  ( T. -> ( x e. CC |-> ( 1 - x ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
15 1 2 2 4 4 6 14 cnmptre 
 |-  ( T. -> ( x e. ( 0 [,] 1 ) |-> ( 1 - x ) ) e. ( II Cn II ) )
16 15 mptru 
 |-  ( x e. ( 0 [,] 1 ) |-> ( 1 - x ) ) e. ( II Cn II )