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

Metamath Proof Explorer

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