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 ⊢ K = J ↾ 𝑡 Y
cnmpt1res.3 ⊢ φ → J ∈ TopOn ⁡ X
cnmpt1res.5 ⊢ φ → Y ⊆ X
cnmpt1res.6 ⊢ φ → x ∈ X ⟼ A ∈ J Cn L
Assertion cnmpt1res ⊢ φ → x ∈ Y ⟼ A ∈ K Cn L

Proof

Step Hyp Ref Expression
1 cnmpt1res.2 ⊢ K = J ↾ 𝑡 Y
2 cnmpt1res.3 ⊢ φ → J ∈ TopOn ⁡ X
3 cnmpt1res.5 ⊢ φ → Y ⊆ X
4 cnmpt1res.6 ⊢ φ → x ∈ X ⟼ A ∈ J Cn L
5 3 resmptd ⊢ φ → x ∈ X ⟼ A ↾ Y = x ∈ Y ⟼ A
6 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
7 2 6 syl ⊢ φ → X = ⋃ J
8 3 7 sseqtrd ⊢ φ → Y ⊆ ⋃ J
9 eqid ⊢ ⋃ J = ⋃ J
10 9 cnrest ⊢ x ∈ X ⟼ A ∈ J Cn L ∧ Y ⊆ ⋃ J → x ∈ X ⟼ A ↾ Y ∈ J ↾ 𝑡 Y Cn L
11 4 8 10 syl2anc ⊢ φ → x ∈ X ⟼ A ↾ Y ∈ J ↾ 𝑡 Y Cn L
12 1 oveq1i ⊢ K Cn L = J ↾ 𝑡 Y Cn L
13 11 12 eleqtrrdi ⊢ φ → x ∈ X ⟼ A ↾ Y ∈ K Cn L
14 5 13 eqeltrrd ⊢ φ → x ∈ Y ⟼ A ∈ K Cn L