Metamath Proof Explorer

Theorem cnmptkc

Description: The curried first projection function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

		Ref	Expression
	Hypotheses	cnmptk1.j	$⊢ φ \to J \in TopOn (X)$
		cnmptk1.k	$⊢ φ \to K \in TopOn (Y)$
	Assertion	cnmptkc	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ x)) \in (J Cn (J^_{ko} K))$

Proof

Step	Hyp	Ref	Expression
1		cnmptk1.j	$⊢ φ \to J \in TopOn (X)$
2		cnmptk1.k	$⊢ φ \to K \in TopOn (Y)$
3		fconstmpt	$⊢ Y \times \{x\} = (y \in Y ⟼ x)$
4	3	mpteq2i	$⊢ (x \in X ⟼ Y \times \{x\}) = (x \in X ⟼ (y \in Y ⟼ x))$
5		xkoccn	$⊢ (K \in TopOn (Y) \land J \in TopOn (X)) \to (x \in X ⟼ Y \times \{x\}) \in (J Cn (J^_{ko} K))$
6	2 1 5	syl2anc	$⊢ φ \to (x \in X ⟼ Y \times \{x\}) \in (J Cn (J^_{ko} K))$
7	4 6	eqeltrrid	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ x)) \in (J Cn (J^_{ko} K))$