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

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	\|- ( ph -> J e. ( TopOn ` X ) )
		cnmptk1.k	\|- ( ph -> K e. ( TopOn ` Y ) )
	Assertion	cnmptkc	\|- ( ph -> ( x e. X \|-> ( y e. Y \|-> x ) ) e. ( J Cn ( J ^ko K ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnmptk1.j	\|- ( ph -> J e. ( TopOn ` X ) )
2		cnmptk1.k	\|- ( ph -> K e. ( TopOn ` Y ) )
3		fconstmpt	\|- ( Y X. { x } ) = ( y e. Y \|-> x )
4	3	mpteq2i	\|- ( x e. X \|-> ( Y X. { x } ) ) = ( x e. X \|-> ( y e. Y \|-> x ) )
5		xkoccn	\|- ( ( K e. ( TopOn ` Y ) /\ J e. ( TopOn ` X ) ) -> ( x e. X \|-> ( Y X. { x } ) ) e. ( J Cn ( J ^ko K ) ) )
6	2 1 5	syl2anc	\|- ( ph -> ( x e. X \|-> ( Y X. { x } ) ) e. ( J Cn ( J ^ko K ) ) )
7	4 6	eqeltrrid	\|- ( ph -> ( x e. X \|-> ( y e. Y \|-> x ) ) e. ( J Cn ( J ^ko K ) ) )