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 ⊢ X = ⋃ J
Assertion hmeocld ⊢ F ∈ J Homeo K ∧ A ⊆ X → A ∈ Clsd ⁡ J ↔ F A ∈ Clsd ⁡ K

Proof

Step Hyp Ref Expression
1 hmeoopn.1 ⊢ X = ⋃ J
2 hmeocnvcn ⊢ F ∈ J Homeo K → F -1 ∈ K Cn J
3 2 adantr ⊢ F ∈ J Homeo K ∧ A ⊆ X → F -1 ∈ K Cn J
4 imacnvcnv ⊢ F -1 -1 A = F A
5 cnclima ⊢ F -1 ∈ K Cn J ∧ A ∈ Clsd ⁡ J → F -1 -1 A ∈ Clsd ⁡ K
6 4 5 eqeltrrid ⊢ F -1 ∈ K Cn J ∧ A ∈ Clsd ⁡ J → F A ∈ Clsd ⁡ K
7 6 ex ⊢ F -1 ∈ K Cn J → A ∈ Clsd ⁡ J → F A ∈ Clsd ⁡ K
8 3 7 syl ⊢ F ∈ J Homeo K ∧ A ⊆ X → A ∈ Clsd ⁡ J → F A ∈ Clsd ⁡ K
9 hmeocn ⊢ F ∈ J Homeo K → F ∈ J Cn K
10 9 adantr ⊢ F ∈ J Homeo K ∧ A ⊆ X → F ∈ J Cn K
11 cnclima ⊢ F ∈ J Cn K ∧ F A ∈ Clsd ⁡ K → F -1 F A ∈ Clsd ⁡ J
12 11 ex ⊢ F ∈ J Cn K → F A ∈ Clsd ⁡ K → F -1 F A ∈ Clsd ⁡ J
13 10 12 syl ⊢ F ∈ J Homeo K ∧ A ⊆ X → F A ∈ Clsd ⁡ K → F -1 F A ∈ Clsd ⁡ J
14 eqid ⊢ ⋃ K = ⋃ K
15 1 14 hmeof1o ⊢ F ∈ J Homeo K → F : X ⟶ 1-1 onto ⋃ K
16 f1of1 ⊢ F : X ⟶ 1-1 onto ⋃ K → F : X ⟶ 1-1 ⋃ K
17 15 16 syl ⊢ F ∈ J Homeo K → F : X ⟶ 1-1 ⋃ K
18 f1imacnv ⊢ F : X ⟶ 1-1 ⋃ K ∧ A ⊆ X → F -1 F A = A
19 17 18 sylan ⊢ F ∈ J Homeo K ∧ A ⊆ X → F -1 F A = A
20 19 eleq1d ⊢ F ∈ J Homeo K ∧ A ⊆ X → F -1 F A ∈ Clsd ⁡ J ↔ A ∈ Clsd ⁡ J
21 13 20 sylibd ⊢ F ∈ J Homeo K ∧ A ⊆ X → F A ∈ Clsd ⁡ K → A ∈ Clsd ⁡ J
22 8 21 impbid ⊢ F ∈ J Homeo K ∧ A ⊆ X → A ∈ Clsd ⁡ J ↔ F A ∈ Clsd ⁡ K