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 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ 𝐽 ↔ ( 𝐹 “ 𝐴 ) ∈ 𝐾 ) )