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

Metamath Proof Explorer

Theorem cnmpt2res

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

Ref Expression
Hypotheses cnmpt1res.2 ⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
cnmpt1res.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
cnmpt1res.5 ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
cnmpt2res.7 ⊢ 𝑁 = ( 𝑀 ↾t 𝑊 )
cnmpt2res.8 ⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ 𝑍 ) )
cnmpt2res.9 ⊢ ( 𝜑 → 𝑊 ⊆ 𝑍 )
cnmpt2res.10 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑍 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝑀 ) Cn 𝐿 ) )
Assertion cnmpt2res ( 𝜑 → ( 𝑥 ∈ 𝑌 , 𝑦 ∈ 𝑊 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝑁 ) Cn 𝐿 ) )

Proof

Step Hyp Ref Expression
1 cnmpt1res.2 ⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
2 cnmpt1res.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 cnmpt1res.5 ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
4 cnmpt2res.7 ⊢ 𝑁 = ( 𝑀 ↾t 𝑊 )
5 cnmpt2res.8 ⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ 𝑍 ) )
6 cnmpt2res.9 ⊢ ( 𝜑 → 𝑊 ⊆ 𝑍 )
7 cnmpt2res.10 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑍 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝑀 ) Cn 𝐿 ) )
8 xpss12 ⊢ ( ( 𝑌 ⊆ 𝑋 ∧ 𝑊 ⊆ 𝑍 ) → ( 𝑌 × 𝑊 ) ⊆ ( 𝑋 × 𝑍 ) )
9 3 6 8 syl2anc ⊢ ( 𝜑 → ( 𝑌 × 𝑊 ) ⊆ ( 𝑋 × 𝑍 ) )
10 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ( TopOn ‘ 𝑍 ) ) → ( 𝐽 ×t 𝑀 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑍 ) ) )
11 2 5 10 syl2anc ⊢ ( 𝜑 → ( 𝐽 ×t 𝑀 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑍 ) ) )
12 toponuni ⊢ ( ( 𝐽 ×t 𝑀 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑍 ) ) → ( 𝑋 × 𝑍 ) = ∪ ( 𝐽 ×t 𝑀 ) )
13 11 12 syl ⊢ ( 𝜑 → ( 𝑋 × 𝑍 ) = ∪ ( 𝐽 ×t 𝑀 ) )
14 9 13 sseqtrd ⊢ ( 𝜑 → ( 𝑌 × 𝑊 ) ⊆ ∪ ( 𝐽 ×t 𝑀 ) )
15 eqid ⊢ ∪ ( 𝐽 ×t 𝑀 ) = ∪ ( 𝐽 ×t 𝑀 )
16 15 cnrest ⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑍 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝑀 ) Cn 𝐿 ) ∧ ( 𝑌 × 𝑊 ) ⊆ ∪ ( 𝐽 ×t 𝑀 ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑌 × 𝑊 ) ) ∈ ( ( ( 𝐽 ×t 𝑀 ) ↾t ( 𝑌 × 𝑊 ) ) Cn 𝐿 ) )
17 7 14 16 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑌 × 𝑊 ) ) ∈ ( ( ( 𝐽 ×t 𝑀 ) ↾t ( 𝑌 × 𝑊 ) ) Cn 𝐿 ) )
18 resmpo ⊢ ( ( 𝑌 ⊆ 𝑋 ∧ 𝑊 ⊆ 𝑍 ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑌 × 𝑊 ) ) = ( 𝑥 ∈ 𝑌 , 𝑦 ∈ 𝑊 ↦ 𝐴 ) )
19 3 6 18 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑌 × 𝑊 ) ) = ( 𝑥 ∈ 𝑌 , 𝑦 ∈ 𝑊 ↦ 𝐴 ) )
20 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
21 2 20 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
22 topontop ⊢ ( 𝑀 ∈ ( TopOn ‘ 𝑍 ) → 𝑀 ∈ Top )
23 5 22 syl ⊢ ( 𝜑 → 𝑀 ∈ Top )
24 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
25 2 24 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
26 25 3 ssexd ⊢ ( 𝜑 → 𝑌 ∈ V )
27 toponmax ⊢ ( 𝑀 ∈ ( TopOn ‘ 𝑍 ) → 𝑍 ∈ 𝑀 )
28 5 27 syl ⊢ ( 𝜑 → 𝑍 ∈ 𝑀 )
29 28 6 ssexd ⊢ ( 𝜑 → 𝑊 ∈ V )
30 txrest ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ Top ) ∧ ( 𝑌 ∈ V ∧ 𝑊 ∈ V ) ) → ( ( 𝐽 ×t 𝑀 ) ↾t ( 𝑌 × 𝑊 ) ) = ( ( 𝐽 ↾t 𝑌 ) ×t ( 𝑀 ↾t 𝑊 ) ) )
31 21 23 26 29 30 syl22anc ⊢ ( 𝜑 → ( ( 𝐽 ×t 𝑀 ) ↾t ( 𝑌 × 𝑊 ) ) = ( ( 𝐽 ↾t 𝑌 ) ×t ( 𝑀 ↾t 𝑊 ) ) )
32 1 4 oveq12i ⊢ ( 𝐾 ×t 𝑁 ) = ( ( 𝐽 ↾t 𝑌 ) ×t ( 𝑀 ↾t 𝑊 ) )
33 31 32 eqtr4di ⊢ ( 𝜑 → ( ( 𝐽 ×t 𝑀 ) ↾t ( 𝑌 × 𝑊 ) ) = ( 𝐾 ×t 𝑁 ) )
34 33 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐽 ×t 𝑀 ) ↾t ( 𝑌 × 𝑊 ) ) Cn 𝐿 ) = ( ( 𝐾 ×t 𝑁 ) Cn 𝐿 ) )
35 17 19 34 3eltr3d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑌 , 𝑦 ∈ 𝑊 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝑁 ) Cn 𝐿 ) )