This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnfdmsn

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

Ref Expression
Assertion cnfdmsn 
|- ( ( A e. V /\ B e. W ) -> ( x e. { A } |-> B ) e. ( ~P { A } Cn ~P { B } ) )

Proof

Step Hyp Ref Expression
1 fmptsnxp 
 |-  ( ( A e. V /\ B e. W ) -> ( x e. { A } |-> B ) = ( { A } X. { B } ) )
2 snex 
 |-  { A } e. _V
3 distopon 
 |-  ( { A } e. _V -> ~P { A } e. ( TopOn ` { A } ) )
4 2 3 mp1i 
 |-  ( ( A e. V /\ B e. W ) -> ~P { A } e. ( TopOn ` { A } ) )
5 snex 
 |-  { B } e. _V
6 distopon 
 |-  ( { B } e. _V -> ~P { B } e. ( TopOn ` { B } ) )
7 5 6 mp1i 
 |-  ( ( A e. V /\ B e. W ) -> ~P { B } e. ( TopOn ` { B } ) )
8 snidg 
 |-  ( B e. W -> B e. { B } )
9 8 adantl 
 |-  ( ( A e. V /\ B e. W ) -> B e. { B } )
10 cnconst2 
 |-  ( ( ~P { A } e. ( TopOn ` { A } ) /\ ~P { B } e. ( TopOn ` { B } ) /\ B e. { B } ) -> ( { A } X. { B } ) e. ( ~P { A } Cn ~P { B } ) )
11 4 7 9 10 syl3anc 
 |-  ( ( A e. V /\ B e. W ) -> ( { A } X. { B } ) e. ( ~P { A } Cn ~P { B } ) )
12 1 11 eqeltrd 
 |-  ( ( A e. V /\ B e. W ) -> ( x e. { A } |-> B ) e. ( ~P { A } Cn ~P { B } ) )