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	$⊢ φ \to J \in TopOn (X)$
	cnmpt21.k	$⊢ φ \to K \in TopOn (Y)$
	cnmpt2c.l	$⊢ φ \to L \in TopOn (Z)$
	cnmpt2c.p	$⊢ φ \to P \in Z$
Assertion	cnmpt2c	$⊢ φ \to (x \in X, y \in Y ⟼ P) \in ((J \times_{t} K) Cn L)$

Step	Hyp	Ref	Expression
1		cnmpt21.j	$⊢ φ \to J \in TopOn (X)$
2		cnmpt21.k	$⊢ φ \to K \in TopOn (Y)$
3		cnmpt2c.l	$⊢ φ \to L \in TopOn (Z)$
4		cnmpt2c.p	$⊢ φ \to P \in Z$
5		eqidd	$⊢ z = ⟨x, y⟩ \to P = P$
6	5	mpompt	$⊢ (z \in (X \times Y) ⟼ P) = (x \in X, y \in Y ⟼ P)$
7		txtopon	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \times_{t} K \in TopOn (X \times Y)$
8	1 2 7	syl2anc	$⊢ φ \to J \times_{t} K \in TopOn (X \times Y)$
9	8 3 4	cnmptc	$⊢ φ \to (z \in (X \times Y) ⟼ P) \in ((J \times_{t} K) Cn L)$
10	6 9	eqeltrrid	$⊢ φ \to (x \in X, y \in Y ⟼ P) \in ((J \times_{t} K) Cn L)$

Metamath Proof Explorer