Metamath Proof Explorer

Theorem cnconst

Description: A constant function is continuous. (Contributed by FL, 15-Jan-2007) (Proof shortened by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion cnconst 
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( B e. Y /\ F : X --> { B } ) ) -> F e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 fconst2g 
 |-  ( B e. Y -> ( F : X --> { B } <-> F = ( X X. { B } ) ) )
2 1 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ B e. Y ) -> ( F : X --> { B } <-> F = ( X X. { B } ) ) )
3 cnconst2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) -> ( X X. { B } ) e. ( J Cn K ) )
4 3 3expa 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ B e. Y ) -> ( X X. { B } ) e. ( J Cn K ) )
5 eleq1 
 |-  ( F = ( X X. { B } ) -> ( F e. ( J Cn K ) <-> ( X X. { B } ) e. ( J Cn K ) ) )
6 4 5 syl5ibrcom 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ B e. Y ) -> ( F = ( X X. { B } ) -> F e. ( J Cn K ) ) )
7 2 6 sylbid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ B e. Y ) -> ( F : X --> { B } -> F e. ( J Cn K ) ) )
8 7 impr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( B e. Y /\ F : X --> { B } ) ) -> F e. ( J Cn K ) )