Metamath Proof Explorer

Theorem hmeocld

Description: Homeomorphisms preserve closedness. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis hmeoopn.1 ⊢ 𝑋 = ∪ 𝐽
Assertion hmeocld ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 hmeoopn.1 ⊢ 𝑋 = ∪ 𝐽
2 hmeocnvcn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) )
3 2 adantr ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) )
4 imacnvcnv ⊢ ( ◡ ◡ 𝐹 “ 𝐴 ) = ( 𝐹 “ 𝐴 )
5 cnclima ⊢ ( ( ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( ◡ ◡ 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐾 ) )
6 4 5 eqeltrrid ⊢ ( ( ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐾 ) )
7 6 ex ⊢ ( ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) → ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) → ( 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐾 ) ) )
8 3 7 syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) → ( 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐾 ) ) )
9 hmeocn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
10 9 adantr ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
11 cnclima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) )
12 11 ex ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( ( 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐾 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) ) )
13 10 12 syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐾 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) ) )
14 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
15 1 14 hmeof1o ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 : 𝑋 –1-1-onto→ ∪ 𝐾 )
16 f1of1 ⊢ ( 𝐹 : 𝑋 –1-1-onto→ ∪ 𝐾 → 𝐹 : 𝑋 –1-1→ ∪ 𝐾 )
17 15 16 syl ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 : 𝑋 –1-1→ ∪ 𝐾 )
18 f1imacnv ⊢ ( ( 𝐹 : 𝑋 –1-1→ ∪ 𝐾 ∧ 𝐴 ⊆ 𝑋 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) = 𝐴 )
19 17 18 sylan ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) = 𝐴 )
20 19 eleq1d ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) ∈ ( Clsd ‘ 𝐽 ) ↔ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
21 13 20 sylibd ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐾 ) → 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
22 8 21 impbid ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝐹 “ 𝐴 ) ∈ ( Clsd ‘ 𝐾 ) ) )