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 e. Top /\ K e. Top /\ F e. ( J Cn K ) ) -> F e. ( J Cn ( K |`t ran F ) ) )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( J e. Top /\ K e. Top /\ F e. ( J Cn K ) ) -> F e. ( J Cn K ) )
2 simp2 
 |-  ( ( J e. Top /\ K e. Top /\ F e. ( J Cn K ) ) -> K e. Top )
3 eqid 
 |-  U. K = U. K
4 3 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
5 2 4 sylib 
 |-  ( ( J e. Top /\ K e. Top /\ F e. ( J Cn K ) ) -> K e. ( TopOn ` U. K ) )
6 ssidd 
 |-  ( ( J e. Top /\ K e. Top /\ F e. ( J Cn K ) ) -> ran F C_ ran F )
7 eqid 
 |-  U. J = U. J
8 7 3 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
9 8 frnd 
 |-  ( F e. ( J Cn K ) -> ran F C_ U. K )
10 9 3ad2ant3 
 |-  ( ( J e. Top /\ K e. Top /\ F e. ( J Cn K ) ) -> ran F C_ U. K )
11 cnrest2 
 |-  ( ( K e. ( TopOn ` U. K ) /\ ran F C_ ran F /\ ran F C_ U. K ) -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K |`t ran F ) ) ) )
12 5 6 10 11 syl3anc 
 |-  ( ( J e. Top /\ K e. Top /\ F e. ( J Cn K ) ) -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K |`t ran F ) ) ) )
13 1 12 mpbid 
 |-  ( ( J e. Top /\ K e. Top /\ F e. ( J Cn K ) ) -> F e. ( J Cn ( K |`t ran F ) ) )