Metamath Proof Explorer

Theorem hmeoimaf1o

Description: The function mapping open sets to their images under a homeomorphism is a bijection of topologies. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Hypothesis hmeoimaf1o.1 ⊢ 𝐺 = ( 𝑥 ∈ 𝐽 ↦ ( 𝐹 “ 𝑥 ) )
Assertion hmeoimaf1o ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐺 : 𝐽 –1-1-onto→ 𝐾 )

Proof

Step Hyp Ref Expression
1 hmeoimaf1o.1 ⊢ 𝐺 = ( 𝑥 ∈ 𝐽 ↦ ( 𝐹 “ 𝑥 ) )
2 hmeoima ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ 𝑥 ) ∈ 𝐾 )
3 hmeocn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
4 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑦 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
5 3 4 sylan ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑦 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
6 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
7 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
8 6 7 hmeof1o ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 : ∪ 𝐽 –1-1-onto→ ∪ 𝐾 )
9 8 adantr ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → 𝐹 : ∪ 𝐽 –1-1-onto→ ∪ 𝐾 )
10 f1of1 ⊢ ( 𝐹 : ∪ 𝐽 –1-1-onto→ ∪ 𝐾 → 𝐹 : ∪ 𝐽 –1-1→ ∪ 𝐾 )
11 9 10 syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → 𝐹 : ∪ 𝐽 –1-1→ ∪ 𝐾 )
12 elssuni ⊢ ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽 )
13 12 ad2antrl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑥 ⊆ ∪ 𝐽 )
14 cnvimass ⊢ ( ◡ 𝐹 “ 𝑦 ) ⊆ dom 𝐹
15 f1dm ⊢ ( 𝐹 : ∪ 𝐽 –1-1→ ∪ 𝐾 → dom 𝐹 = ∪ 𝐽 )
16 11 15 syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → dom 𝐹 = ∪ 𝐽 )
17 14 16 sseqtrid ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → ( ◡ 𝐹 “ 𝑦 ) ⊆ ∪ 𝐽 )
18 f1imaeq ⊢ ( ( 𝐹 : ∪ 𝐽 –1-1→ ∪ 𝐾 ∧ ( 𝑥 ⊆ ∪ 𝐽 ∧ ( ◡ 𝐹 “ 𝑦 ) ⊆ ∪ 𝐽 ) ) → ( ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ↔ 𝑥 = ( ◡ 𝐹 “ 𝑦 ) ) )
19 11 13 17 18 syl12anc ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ↔ 𝑥 = ( ◡ 𝐹 “ 𝑦 ) ) )
20 f1ofo ⊢ ( 𝐹 : ∪ 𝐽 –1-1-onto→ ∪ 𝐾 → 𝐹 : ∪ 𝐽 –onto→ ∪ 𝐾 )
21 9 20 syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → 𝐹 : ∪ 𝐽 –onto→ ∪ 𝐾 )
22 elssuni ⊢ ( 𝑦 ∈ 𝐾 → 𝑦 ⊆ ∪ 𝐾 )
23 22 ad2antll ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑦 ⊆ ∪ 𝐾 )
24 foimacnv ⊢ ( ( 𝐹 : ∪ 𝐽 –onto→ ∪ 𝐾 ∧ 𝑦 ⊆ ∪ 𝐾 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 )
25 21 23 24 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 )
26 25 eqeq2d ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ↔ ( 𝐹 “ 𝑥 ) = 𝑦 ) )
27 eqcom ⊢ ( ( 𝐹 “ 𝑥 ) = 𝑦 ↔ 𝑦 = ( 𝐹 “ 𝑥 ) )
28 26 27 bitrdi ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ↔ 𝑦 = ( 𝐹 “ 𝑥 ) ) )
29 19 28 bitr3d ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) ↔ 𝑦 = ( 𝐹 “ 𝑥 ) ) )
30 1 2 5 29 f1o2d ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐺 : 𝐽 –1-1-onto→ 𝐾 )