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 ⊢ F ∈ J Homeo K → F -1 ∈ K Homeo J

Proof

Step Hyp Ref Expression
1 hmeocnvcn ⊢ F ∈ J Homeo K → F -1 ∈ K Cn J
2 hmeocn ⊢ F ∈ J Homeo K → F ∈ J Cn K
3 eqid ⊢ ⋃ J = ⋃ J
4 eqid ⊢ ⋃ K = ⋃ K
5 3 4 cnf ⊢ F ∈ J Cn K → F : ⋃ J ⟶ ⋃ K
6 frel ⊢ F : ⋃ J ⟶ ⋃ K → Rel ⁡ F
7 2 5 6 3syl ⊢ F ∈ J Homeo K → Rel ⁡ F
8 dfrel2 ⊢ Rel ⁡ F ↔ F -1 -1 = F
9 7 8 sylib ⊢ F ∈ J Homeo K → F -1 -1 = F
10 9 2 eqeltrd ⊢ F ∈ J Homeo K → F -1 -1 ∈ J Cn K
11 ishmeo ⊢ F -1 ∈ K Homeo J ↔ F -1 ∈ K Cn J ∧ F -1 -1 ∈ J Cn K
12 1 10 11 sylanbrc ⊢ F ∈ J Homeo K → F -1 ∈ K Homeo J