Theorem cnresima

Description: A continuous function is continuous onto its image. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 15-Dec-2013)

	Ref	Expression
Assertion	cnresima	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t ran 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp3	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
2		simp2	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ Top )
3		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
4	3	toptopon	⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
5	2 4	sylib	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
6		ssidd	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ran 𝐹 ⊆ ran 𝐹 )
7		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
8	7 3	cnf	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
9	8	frnd	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ran 𝐹 ⊆ ∪ 𝐾 )
10	9	3ad2ant3	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ran 𝐹 ⊆ ∪ 𝐾 )
11		cnrest2	⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ ran 𝐹 ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ ∪ 𝐾 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t ran 𝐹 ) ) ) )
12	5 6 10 11	syl3anc	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t ran 𝐹 ) ) ) )
13	1 12	mpbid	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐾 ↾t ran 𝐹 ) ) )