Metamath Proof Explorer

Theorem hmphref

Description: "Is homeomorphic to" is reflexive. (Contributed by FL, 25-Feb-2007) (Proof shortened by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion hmphref 
|- ( J e. Top -> J ~= J )

Proof

Step Hyp Ref Expression
1 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
2 idhmeo 
 |-  ( J e. ( TopOn ` U. J ) -> ( _I |` U. J ) e. ( J Homeo J ) )
3 1 2 sylbi 
 |-  ( J e. Top -> ( _I |` U. J ) e. ( J Homeo J ) )
4 hmphi 
 |-  ( ( _I |` U. J ) e. ( J Homeo J ) -> J ~= J )
5 3 4 syl 
 |-  ( J e. Top -> J ~= J )