Metamath Proof Explorer

Theorem ishmeo

Description: The predicate F is a homeomorphism between topology J and topology K . Criterion of BourbakiTop1 p. I.2. (Contributed by FL, 14-Feb-2007) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion ishmeo ⊢ F ∈ J Homeo K ↔ F ∈ J Cn K ∧ F -1 ∈ K Cn J

Proof

Step Hyp Ref Expression
1 cnveq ⊢ f = F → f -1 = F -1
2 1 eleq1d ⊢ f = F → f -1 ∈ K Cn J ↔ F -1 ∈ K Cn J
3 hmeofval ⊢ J Homeo K = f ∈ J Cn K | f -1 ∈ K Cn J
4 2 3 elrab2 ⊢ F ∈ J Homeo K ↔ F ∈ J Cn K ∧ F -1 ∈ K Cn J