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