Metamath Proof Explorer

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	$⊢ (J \in Top \land K \in Top \land F \in (J Cn K)) \to F \in (J Cn (K ↾_{𝑡} ran F))$

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (J \in Top \land K \in Top \land F \in (J Cn K)) \to F \in (J Cn K)$
2		simp2	$⊢ (J \in Top \land K \in Top \land F \in (J Cn K)) \to K \in Top$
3		eqid	$⊢ ⋃ K = ⋃ K$
4	3	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
5	2 4	sylib	$⊢ (J \in Top \land K \in Top \land F \in (J Cn K)) \to K \in TopOn (⋃ K)$
6		ssidd	$⊢ (J \in Top \land K \in Top \land F \in (J Cn K)) \to ran F \subseteq ran F$
7		eqid	$⊢ ⋃ J = ⋃ J$
8	7 3	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ ⋃ K$
9	8	frnd	$⊢ F \in (J Cn K) \to ran F \subseteq ⋃ K$
10	9	3ad2ant3	$⊢ (J \in Top \land K \in Top \land F \in (J Cn K)) \to ran F \subseteq ⋃ K$
11		cnrest2	$⊢ (K \in TopOn (⋃ K) \land ran F \subseteq ran F \land ran F \subseteq ⋃ K) \to (F \in (J Cn K) \leftrightarrow F \in (J Cn (K ↾_{𝑡} ran F)))$
12	5 6 10 11	syl3anc	$⊢ (J \in Top \land K \in Top \land F \in (J Cn K)) \to (F \in (J Cn K) \leftrightarrow F \in (J Cn (K ↾_{𝑡} ran F)))$
13	1 12	mpbid	$⊢ (J \in Top \land K \in Top \land F \in (J Cn K)) \to F \in (J Cn (K ↾_{𝑡} ran F))$