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