Theorem cnmpt2c

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

	Ref	Expression
Hypotheses	cnmpt21.j	|- ( ph -> J e. ( TopOn ` X ) )
	cnmpt21.k	|- ( ph -> K e. ( TopOn ` Y ) )
	cnmpt2c.l	|- ( ph -> L e. ( TopOn ` Z ) )
	cnmpt2c.p	|- ( ph -> P e. Z )
Assertion	cnmpt2c	|- ( ph -> ( x e. X , y e. Y |-> P ) e. ( ( J tX K ) Cn L ) )

Proof

Step	Hyp	Ref	Expression
1		cnmpt21.j	|- ( ph -> J e. ( TopOn ` X ) )
2		cnmpt21.k	|- ( ph -> K e. ( TopOn ` Y ) )
3		cnmpt2c.l	|- ( ph -> L e. ( TopOn ` Z ) )
4		cnmpt2c.p	|- ( ph -> P e. Z )
5		eqidd	|- ( z = <. x , y >. -> P = P )
6	5	mpompt	|- ( z e. ( X X. Y ) |-> P ) = ( x e. X , y e. Y |-> P )
7		txtopon	|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
8	1 2 7	syl2anc	|- ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
9	8 3 4	cnmptc	|- ( ph -> ( z e. ( X X. Y ) |-> P ) e. ( ( J tX K ) Cn L ) )
10	6 9	eqeltrrid	|- ( ph -> ( x e. X , y e. Y |-> P ) e. ( ( J tX K ) Cn L ) )