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

Metamath Proof Explorer

Theorem hmeocnv

Description: The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion hmeocnv ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Homeo 𝐽 ) )

Proof

Step Hyp Ref Expression
1 hmeocnvcn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) )
2 hmeocn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
4 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
5 3 4 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
6 frel ⊢ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 → Rel 𝐹 )
7 2 5 6 3syl ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → Rel 𝐹 )
8 dfrel2 ⊢ ( Rel 𝐹 ↔ ◡ ◡ 𝐹 = 𝐹 )
9 7 8 sylib ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ ◡ 𝐹 = 𝐹 )
10 9 2 eqeltrd ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ ◡ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
11 ishmeo ⊢ ( ◡ 𝐹 ∈ ( 𝐾 Homeo 𝐽 ) ↔ ( ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ∧ ◡ ◡ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) )
12 1 10 11 sylanbrc ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Homeo 𝐽 ) )