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	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
3	1 2	cnf	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
4	3	adantr	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐾 ) ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
5		ffun	⊢ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 → Fun 𝐹 )
6		funcnvcnv	⊢ ( Fun 𝐹 → Fun ◡ ◡ 𝐹 )
7		imadif	⊢ ( Fun ◡ ◡ 𝐹 → ( ◡ 𝐹 “ ( ∪ 𝐾 ∖ 𝐴 ) ) = ( ( ◡ 𝐹 “ ∪ 𝐾 ) ∖ ( ◡ 𝐹 “ 𝐴 ) ) )
8	5 6 7	3syl	⊢ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 → ( ◡ 𝐹 “ ( ∪ 𝐾 ∖ 𝐴 ) ) = ( ( ◡ 𝐹 “ ∪ 𝐾 ) ∖ ( ◡ 𝐹 “ 𝐴 ) ) )
9		fimacnv	⊢ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 → ( ◡ 𝐹 “ ∪ 𝐾 ) = ∪ 𝐽 )
10	9	difeq1d	⊢ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 → ( ( ◡ 𝐹 “ ∪ 𝐾 ) ∖ ( ◡ 𝐹 “ 𝐴 ) ) = ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝐴 ) ) )
11	8 10	eqtr2d	⊢ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 → ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝐴 ) ) = ( ◡ 𝐹 “ ( ∪ 𝐾 ∖ 𝐴 ) ) )
12	4 11	syl	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐾 ) ) → ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝐴 ) ) = ( ◡ 𝐹 “ ( ∪ 𝐾 ∖ 𝐴 ) ) )
13	2	cldopn	⊢ ( 𝐴 ∈ ( Clsd ‘ 𝐾 ) → ( ∪ 𝐾 ∖ 𝐴 ) ∈ 𝐾 )
14		cnima	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( ∪ 𝐾 ∖ 𝐴 ) ∈ 𝐾 ) → ( ◡ 𝐹 “ ( ∪ 𝐾 ∖ 𝐴 ) ) ∈ 𝐽 )
15	13 14	sylan2	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ ( ∪ 𝐾 ∖ 𝐴 ) ) ∈ 𝐽 )
16	12 15	eqeltrd	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐾 ) ) → ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝐴 ) ) ∈ 𝐽 )
17		cntop1	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
18		cnvimass	⊢ ( ◡ 𝐹 “ 𝐴 ) ⊆ dom 𝐹
19	18 4	fssdm	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ 𝐴 ) ⊆ ∪ 𝐽 )
20	1	iscld2	⊢ ( ( 𝐽 ∈ Top ∧ ( ◡ 𝐹 “ 𝐴 ) ⊆ ∪ 𝐽 ) → ( ( ◡ 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) ↔ ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝐴 ) ) ∈ 𝐽 ) )
21	17 19 20	syl2an2r	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐾 ) ) → ( ( ◡ 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) ↔ ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝐴 ) ) ∈ 𝐽 ) )
22	16 21	mpbird	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) )