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	⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
	cnmpt1res.3	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	cnmpt1res.5	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
	cnmpt1res.6	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐿 ) )
Assertion	cnmpt1res	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		cnmpt1res.2	⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
2		cnmpt1res.3	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3		cnmpt1res.5	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
4		cnmpt1res.6	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐿 ) )
5	3	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑌 ) = ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) )
6		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
7	2 6	syl	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
8	3 7	sseqtrd	⊢ ( 𝜑 → 𝑌 ⊆ ∪ 𝐽 )
9		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
10	9	cnrest	⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐿 ) ∧ 𝑌 ⊆ ∪ 𝐽 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑌 ) ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐿 ) )
11	4 8 10	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑌 ) ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐿 ) )
12	1	oveq1i	⊢ ( 𝐾 Cn 𝐿 ) = ( ( 𝐽 ↾t 𝑌 ) Cn 𝐿 )
13	11 12	eleqtrrdi	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ↾ 𝑌 ) ∈ ( 𝐾 Cn 𝐿 ) )
14	5 13	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑌 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐿 ) )