Metamath Proof Explorer

Theorem hmeocls

Description: Homeomorphisms preserve closures. (Contributed by Mario Carneiro, 25-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 hmeoopn.1 ⊢ 𝑋 = ∪ 𝐽
2 hmeocnvcn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) )
3 1 cncls2i ⊢ ( ( ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐾 ) ‘ ( ◡ ◡ 𝐹 “ 𝐴 ) ) ⊆ ( ◡ ◡ 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
4 2 3 sylan ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐾 ) ‘ ( ◡ ◡ 𝐹 “ 𝐴 ) ) ⊆ ( ◡ ◡ 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
5 imacnvcnv ⊢ ( ◡ ◡ 𝐹 “ 𝐴 ) = ( 𝐹 “ 𝐴 )
6 5 fveq2i ⊢ ( ( cls ‘ 𝐾 ) ‘ ( ◡ ◡ 𝐹 “ 𝐴 ) ) = ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) )
7 imacnvcnv ⊢ ( ◡ ◡ 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) = ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
8 4 6 7 3sstr3g ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) ⊆ ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
9 hmeocn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
10 1 cnclsi ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) )
11 9 10 sylan ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) )
12 8 11 eqssd ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝐴 ) ) = ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )