Metamath Proof Explorer

Theorem hmeocnvb

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

Ref Expression
Assertion hmeocnvb ⊢ Rel ⁡ F → F -1 ∈ J Homeo K ↔ F ∈ K Homeo J

Proof

Step Hyp Ref Expression
1 hmeocnv ⊢ F -1 ∈ J Homeo K → F -1 -1 ∈ K Homeo J
2 dfrel2 ⊢ Rel ⁡ F ↔ F -1 -1 = F
3 eleq1 ⊢ F -1 -1 = F → F -1 -1 ∈ K Homeo J ↔ F ∈ K Homeo J
4 2 3 sylbi ⊢ Rel ⁡ F → F -1 -1 ∈ K Homeo J ↔ F ∈ K Homeo J
5 1 4 syl5ib ⊢ Rel ⁡ F → F -1 ∈ J Homeo K → F ∈ K Homeo J
6 hmeocnv ⊢ F ∈ K Homeo J → F -1 ∈ J Homeo K
7 5 6 impbid1 ⊢ Rel ⁡ F → F -1 ∈ J Homeo K ↔ F ∈ K Homeo J