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 ∈ J Cn K ∧ A ∈ Clsd ⁡ K → F -1 A ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 eqid ⊢ ⋃ K = ⋃ K
3 1 2 cnf ⊢ F ∈ J Cn K → F : ⋃ J ⟶ ⋃ K
4 3 adantr ⊢ F ∈ J Cn K ∧ A ∈ Clsd ⁡ K → F : ⋃ J ⟶ ⋃ K
5 ffun ⊢ F : ⋃ J ⟶ ⋃ K → Fun ⁡ F
6 funcnvcnv ⊢ Fun ⁡ F → Fun ⁡ F -1 -1
7 imadif ⊢ Fun ⁡ F -1 -1 → F -1 ⋃ K ∖ A = F -1 ⋃ K ∖ F -1 A
8 5 6 7 3syl ⊢ F : ⋃ J ⟶ ⋃ K → F -1 ⋃ K ∖ A = F -1 ⋃ K ∖ F -1 A
9 fimacnv ⊢ F : ⋃ J ⟶ ⋃ K → F -1 ⋃ K = ⋃ J
10 9 difeq1d ⊢ F : ⋃ J ⟶ ⋃ K → F -1 ⋃ K ∖ F -1 A = ⋃ J ∖ F -1 A
11 8 10 eqtr2d ⊢ F : ⋃ J ⟶ ⋃ K → ⋃ J ∖ F -1 A = F -1 ⋃ K ∖ A
12 4 11 syl ⊢ F ∈ J Cn K ∧ A ∈ Clsd ⁡ K → ⋃ J ∖ F -1 A = F -1 ⋃ K ∖ A
13 2 cldopn ⊢ A ∈ Clsd ⁡ K → ⋃ K ∖ A ∈ K
14 cnima ⊢ F ∈ J Cn K ∧ ⋃ K ∖ A ∈ K → F -1 ⋃ K ∖ A ∈ J
15 13 14 sylan2 ⊢ F ∈ J Cn K ∧ A ∈ Clsd ⁡ K → F -1 ⋃ K ∖ A ∈ J
16 12 15 eqeltrd ⊢ F ∈ J Cn K ∧ A ∈ Clsd ⁡ K → ⋃ J ∖ F -1 A ∈ J
17 cntop1 ⊢ F ∈ J Cn K → J ∈ Top
18 cnvimass ⊢ F -1 A ⊆ dom ⁡ F
19 18 4 fssdm ⊢ F ∈ J Cn K ∧ A ∈ Clsd ⁡ K → F -1 A ⊆ ⋃ J
20 1 iscld2 ⊢ J ∈ Top ∧ F -1 A ⊆ ⋃ J → F -1 A ∈ Clsd ⁡ J ↔ ⋃ J ∖ F -1 A ∈ J
21 17 19 20 syl2an2r ⊢ F ∈ J Cn K ∧ A ∈ Clsd ⁡ K → F -1 A ∈ Clsd ⁡ J ↔ ⋃ J ∖ F -1 A ∈ J
22 16 21 mpbird ⊢ F ∈ J Cn K ∧ A ∈ Clsd ⁡ K → F -1 A ∈ Clsd ⁡ J