This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∪ 𝐽
Assertion hmeoopn ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ 𝐽 ↔ ( 𝐹 “ 𝐴 ) ∈ 𝐾 ) )

Proof

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