This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnclima

Description: A closed subset of the codomain of a continuous function has a closed preimage. (Contributed by NM, 15-Mar-2007) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnclima 
|- ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( `' F " A ) e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 eqid 
 |-  U. K = U. K
3 1 2 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
4 3 adantr 
 |-  ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> F : U. J --> U. K )
5 ffun 
 |-  ( F : U. J --> U. K -> Fun F )
6 funcnvcnv 
 |-  ( Fun F -> Fun `' `' F )
7 imadif 
 |-  ( Fun `' `' F -> ( `' F " ( U. K \ A ) ) = ( ( `' F " U. K ) \ ( `' F " A ) ) )
8 5 6 7 3syl 
 |-  ( F : U. J --> U. K -> ( `' F " ( U. K \ A ) ) = ( ( `' F " U. K ) \ ( `' F " A ) ) )
9 fimacnv 
 |-  ( F : U. J --> U. K -> ( `' F " U. K ) = U. J )
10 9 difeq1d 
 |-  ( F : U. J --> U. K -> ( ( `' F " U. K ) \ ( `' F " A ) ) = ( U. J \ ( `' F " A ) ) )
11 8 10 eqtr2d 
 |-  ( F : U. J --> U. K -> ( U. J \ ( `' F " A ) ) = ( `' F " ( U. K \ A ) ) )
12 4 11 syl 
 |-  ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( U. J \ ( `' F " A ) ) = ( `' F " ( U. K \ A ) ) )
13 2 cldopn 
 |-  ( A e. ( Clsd ` K ) -> ( U. K \ A ) e. K )
14 cnima 
 |-  ( ( F e. ( J Cn K ) /\ ( U. K \ A ) e. K ) -> ( `' F " ( U. K \ A ) ) e. J )
15 13 14 sylan2 
 |-  ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( `' F " ( U. K \ A ) ) e. J )
16 12 15 eqeltrd 
 |-  ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( U. J \ ( `' F " A ) ) e. J )
17 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
18 cnvimass 
 |-  ( `' F " A ) C_ dom F
19 18 4 fssdm 
 |-  ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( `' F " A ) C_ U. J )
20 1 iscld2 
 |-  ( ( J e. Top /\ ( `' F " A ) C_ U. J ) -> ( ( `' F " A ) e. ( Clsd ` J ) <-> ( U. J \ ( `' F " A ) ) e. J ) )
21 17 19 20 syl2an2r 
 |-  ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( ( `' F " A ) e. ( Clsd ` J ) <-> ( U. J \ ( `' F " A ) ) e. J ) )
22 16 21 mpbird 
 |-  ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( `' F " A ) e. ( Clsd ` J ) )