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

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