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 ) )