Metamath Proof Explorer

Theorem hmeocls

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

Ref Expression
Hypothesis hmeoopn.1 ⊢ X = ⋃ J
Assertion hmeocls ⊢ F ∈ J Homeo K ∧ A ⊆ X → cls ⁡ K ⁡ F A = F cls ⁡ J ⁡ A

Proof

Step Hyp Ref Expression
1 hmeoopn.1 ⊢ X = ⋃ J
2 hmeocnvcn ⊢ F ∈ J Homeo K → F -1 ∈ K Cn J
3 1 cncls2i ⊢ F -1 ∈ K Cn J ∧ A ⊆ X → cls ⁡ K ⁡ F -1 -1 A ⊆ F -1 -1 cls ⁡ J ⁡ A
4 2 3 sylan ⊢ F ∈ J Homeo K ∧ A ⊆ X → cls ⁡ K ⁡ F -1 -1 A ⊆ F -1 -1 cls ⁡ J ⁡ A
5 imacnvcnv ⊢ F -1 -1 A = F A
6 5 fveq2i ⊢ cls ⁡ K ⁡ F -1 -1 A = cls ⁡ K ⁡ F A
7 imacnvcnv ⊢ F -1 -1 cls ⁡ J ⁡ A = F cls ⁡ J ⁡ A
8 4 6 7 3sstr3g ⊢ F ∈ J Homeo K ∧ A ⊆ X → cls ⁡ K ⁡ F A ⊆ F cls ⁡ J ⁡ A
9 hmeocn ⊢ F ∈ J Homeo K → F ∈ J Cn K
10 1 cnclsi ⊢ F ∈ J Cn K ∧ A ⊆ X → F cls ⁡ J ⁡ A ⊆ cls ⁡ K ⁡ F A
11 9 10 sylan ⊢ F ∈ J Homeo K ∧ A ⊆ X → F cls ⁡ J ⁡ A ⊆ cls ⁡ K ⁡ F A
12 8 11 eqssd ⊢ F ∈ J Homeo K ∧ A ⊆ X → cls ⁡ K ⁡ F A = F cls ⁡ J ⁡ A