Metamath Proof Explorer

Theorem hmeoopn

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

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

Proof

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