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 ( ( 𝐹 ∈ ( 𝐽 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 ‘ 𝐽 ) )