Metamath Proof Explorer

Theorem cncfdmsn

Description: A complex function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion cncfdmsn 
|- ( ( A e. CC /\ B e. CC ) -> ( x e. { A } |-> B ) e. ( { A } -cn-> { B } ) )

Proof

Step Hyp Ref Expression
1 cnfdmsn 
 |-  ( ( A e. CC /\ B e. CC ) -> ( x e. { A } |-> B ) e. ( ~P { A } Cn ~P { B } ) )
2 snssi 
 |-  ( A e. CC -> { A } C_ CC )
3 snssi 
 |-  ( B e. CC -> { B } C_ CC )
4 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
5 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t { A } ) = ( ( TopOpen ` CCfld ) |`t { A } )
6 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t { B } ) = ( ( TopOpen ` CCfld ) |`t { B } )
7 4 5 6 cncfcn 
 |-  ( ( { A } C_ CC /\ { B } C_ CC ) -> ( { A } -cn-> { B } ) = ( ( ( TopOpen ` CCfld ) |`t { A } ) Cn ( ( TopOpen ` CCfld ) |`t { B } ) ) )
8 2 3 7 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( { A } -cn-> { B } ) = ( ( ( TopOpen ` CCfld ) |`t { A } ) Cn ( ( TopOpen ` CCfld ) |`t { B } ) ) )
9 4 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
10 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
11 restsn2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ A e. CC ) -> ( ( TopOpen ` CCfld ) |`t { A } ) = ~P { A } )
12 9 10 11 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( TopOpen ` CCfld ) |`t { A } ) = ~P { A } )
13 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
14 restsn2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ B e. CC ) -> ( ( TopOpen ` CCfld ) |`t { B } ) = ~P { B } )
15 9 13 14 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( TopOpen ` CCfld ) |`t { B } ) = ~P { B } )
16 12 15 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( TopOpen ` CCfld ) |`t { A } ) Cn ( ( TopOpen ` CCfld ) |`t { B } ) ) = ( ~P { A } Cn ~P { B } ) )
17 8 16 eqtr2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ~P { A } Cn ~P { B } ) = ( { A } -cn-> { B } ) )
18 1 17 eleqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( x e. { A } |-> B ) e. ( { A } -cn-> { B } ) )