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