Theorem cnmptc

Description: A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	cnmptid.j	|- ( ph -> J e. ( TopOn ` X ) )
	cnmptc.k	|- ( ph -> K e. ( TopOn ` Y ) )
	cnmptc.p	|- ( ph -> P e. Y )
Assertion	cnmptc	|- ( ph -> ( x e. X |-> P ) e. ( J Cn K ) )

Proof

Step	Hyp	Ref	Expression
1		cnmptid.j	|- ( ph -> J e. ( TopOn ` X ) )
2		cnmptc.k	|- ( ph -> K e. ( TopOn ` Y ) )
3		cnmptc.p	|- ( ph -> P e. Y )
4		fconstmpt	|- ( X X. { P } ) = ( x e. X |-> P )
5		cnconst2	|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. Y ) -> ( X X. { P } ) e. ( J Cn K ) )
6	1 2 3 5	syl3anc	|- ( ph -> ( X X. { P } ) e. ( J Cn K ) )
7	4 6	eqeltrrid	|- ( ph -> ( x e. X |-> P ) e. ( J Cn K ) )