Theorem cnres2

Description: The restriction of a continuous function to a subset is continuous. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 15-Dec-2013)

	Ref	Expression
Hypotheses	cnres2.1	⊢ 𝑋 = ∪ 𝐽
	cnres2.2	⊢ 𝑌 = ∪ 𝐾
Assertion	cnres2	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn ( 𝐾 ↾t 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnres2.1	⊢ 𝑋 = ∪ 𝐽
2		cnres2.2	⊢ 𝑌 = ∪ 𝐾
3		simp3l	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
4		simp2l	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → 𝐴 ⊆ 𝑋 )
5	1	cnrest	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) )
6	3 4 5	syl2anc	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) )
7		simp1r	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → 𝐾 ∈ Top )
8	2	toptopon	⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
9	7 8	sylib	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
10		df-ima	⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
11		simp3r	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
12	1 2	cnf	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
13		ffun	⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → Fun 𝐹 )
14	3 12 13	3syl	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → Fun 𝐹 )
15		fdm	⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → dom 𝐹 = 𝑋 )
16	3 12 15	3syl	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → dom 𝐹 = 𝑋 )
17	4 16	sseqtrrd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → 𝐴 ⊆ dom 𝐹 )
18		funimass4	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
19	14 17 18	syl2anc	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
20	11 19	mpbird	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → ( 𝐹 “ 𝐴 ) ⊆ 𝐵 )
21	10 20	eqsstrrid	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → ran ( 𝐹 ↾ 𝐴 ) ⊆ 𝐵 )
22		simp2r	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → 𝐵 ⊆ 𝑌 )
23		cnrest2	⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran ( 𝐹 ↾ 𝐴 ) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌 ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) ↔ ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn ( 𝐾 ↾t 𝐵 ) ) ) )
24	9 21 22 23	syl3anc	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) ↔ ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn ( 𝐾 ↾t 𝐵 ) ) ) )
25	6 24	mpbid	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ∧ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn ( 𝐾 ↾t 𝐵 ) ) )