Theorem cnmpt1res

Description: The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 5-Jun-2014)

	Ref	Expression
Hypotheses	cnmpt1res.2	|- K = ( J |`t Y )
	cnmpt1res.3	|- ( ph -> J e. ( TopOn ` X ) )
	cnmpt1res.5	|- ( ph -> Y C_ X )
	cnmpt1res.6	|- ( ph -> ( x e. X |-> A ) e. ( J Cn L ) )
Assertion	cnmpt1res	|- ( ph -> ( x e. Y |-> A ) e. ( K Cn L ) )

Proof

Step	Hyp	Ref	Expression
1		cnmpt1res.2	|- K = ( J |`t Y )
2		cnmpt1res.3	|- ( ph -> J e. ( TopOn ` X ) )
3		cnmpt1res.5	|- ( ph -> Y C_ X )
4		cnmpt1res.6	|- ( ph -> ( x e. X |-> A ) e. ( J Cn L ) )
5	3	resmptd	|- ( ph -> ( ( x e. X |-> A ) |` Y ) = ( x e. Y |-> A ) )
6		toponuni	|- ( J e. ( TopOn ` X ) -> X = U. J )
7	2 6	syl	|- ( ph -> X = U. J )
8	3 7	sseqtrd	|- ( ph -> Y C_ U. J )
9		eqid	|- U. J = U. J
10	9	cnrest	|- ( ( ( x e. X |-> A ) e. ( J Cn L ) /\ Y C_ U. J ) -> ( ( x e. X |-> A ) |` Y ) e. ( ( J |`t Y ) Cn L ) )
11	4 8 10	syl2anc	|- ( ph -> ( ( x e. X |-> A ) |` Y ) e. ( ( J |`t Y ) Cn L ) )
12	1	oveq1i	|- ( K Cn L ) = ( ( J |`t Y ) Cn L )
13	11 12	eleqtrrdi	|- ( ph -> ( ( x e. X |-> A ) |` Y ) e. ( K Cn L ) )
14	5 13	eqeltrrd	|- ( ph -> ( x e. Y |-> A ) e. ( K Cn L ) )