Metamath Proof Explorer


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 ) )