Metamath Proof Explorer

Theorem cncfmptc

Description: A constant function is a continuous function on CC . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 7-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
2 1 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
3 simp2 
 |-  ( ( A e. T /\ S C_ CC /\ T C_ CC ) -> S C_ CC )
4 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
5 2 3 4 sylancr 
 |-  ( ( A e. T /\ S C_ CC /\ T C_ CC ) -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
6 simp3 
 |-  ( ( A e. T /\ S C_ CC /\ T C_ CC ) -> T C_ CC )
7 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ T C_ CC ) -> ( ( TopOpen ` CCfld ) |`t T ) e. ( TopOn ` T ) )
8 2 6 7 sylancr 
 |-  ( ( A e. T /\ S C_ CC /\ T C_ CC ) -> ( ( TopOpen ` CCfld ) |`t T ) e. ( TopOn ` T ) )
9 simp1 
 |-  ( ( A e. T /\ S C_ CC /\ T C_ CC ) -> A e. T )
10 5 8 9 cnmptc 
 |-  ( ( A e. T /\ S C_ CC /\ T C_ CC ) -> ( x e. S |-> A ) e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( ( TopOpen ` CCfld ) |`t T ) ) )
11 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
12 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t T ) = ( ( TopOpen ` CCfld ) |`t T )
13 1 11 12 cncfcn 
 |-  ( ( S C_ CC /\ T C_ CC ) -> ( S -cn-> T ) = ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( ( TopOpen ` CCfld ) |`t T ) ) )
14 13 3adant1 
 |-  ( ( A e. T /\ S C_ CC /\ T C_ CC ) -> ( S -cn-> T ) = ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( ( TopOpen ` CCfld ) |`t T ) ) )
15 10 14 eleqtrrd 
 |-  ( ( A e. T /\ S C_ CC /\ T C_ CC ) -> ( x e. S |-> A ) e. ( S -cn-> T ) )