Metamath Proof Explorer

Theorem cncfmptid

Description: The identity function is a continuous function on CC . (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 17-May-2016)

Ref Expression
Assertion cncfmptid 
|- ( ( S C_ T /\ T C_ CC ) -> ( x e. S |-> x ) e. ( S -cn-> T ) )

Proof

Step Hyp Ref Expression
1 cncfss 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( S -cn-> S ) C_ ( S -cn-> T ) )
2 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3 2 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
4 sstr 
 |-  ( ( S C_ T /\ T C_ CC ) -> S C_ CC )
5 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
6 3 4 5 sylancr 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
7 6 cnmptid 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( x e. S |-> x ) e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( ( TopOpen ` CCfld ) |`t S ) ) )
8 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
9 2 8 8 cncfcn 
 |-  ( ( S C_ CC /\ S C_ CC ) -> ( S -cn-> S ) = ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( ( TopOpen ` CCfld ) |`t S ) ) )
10 4 4 9 syl2anc 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( S -cn-> S ) = ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( ( TopOpen ` CCfld ) |`t S ) ) )
11 7 10 eleqtrrd 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( x e. S |-> x ) e. ( S -cn-> S ) )
12 1 11 sseldd 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( x e. S |-> x ) e. ( S -cn-> T ) )