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 φ J TopOn X
cnmpt21.k φ K TopOn Y
cnmpt2c.l φ L TopOn Z
cnmpt2c.p φ P Z
Assertion cnmpt2c φ x X , y Y P J × t K Cn L

Proof

Step Hyp Ref Expression
1 cnmpt21.j φ J TopOn X
2 cnmpt21.k φ K TopOn Y
3 cnmpt2c.l φ L TopOn Z
4 cnmpt2c.p φ P Z
5 eqidd z = x y P = P
6 5 mpompt z X × Y P = x X , y Y P
7 txtopon J TopOn X K TopOn Y J × t K TopOn X × Y
8 1 2 7 syl2anc φ J × t K TopOn X × Y
9 8 3 4 cnmptc φ z X × Y P J × t K Cn L
10 6 9 eqeltrrid φ x X , y Y P J × t K Cn L