Metamath Proof Explorer

Theorem idhmeo

Description: The identity function is a homeomorphism. (Contributed by FL, 14-Feb-2007) (Proof shortened by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion idhmeo 
|- ( J e. ( TopOn ` X ) -> ( _I |` X ) e. ( J Homeo J ) )

Proof

Step Hyp Ref Expression
1 idcn 
 |-  ( J e. ( TopOn ` X ) -> ( _I |` X ) e. ( J Cn J ) )
2 cnvresid 
 |-  `' ( _I |` X ) = ( _I |` X )
3 2 1 eqeltrid 
 |-  ( J e. ( TopOn ` X ) -> `' ( _I |` X ) e. ( J Cn J ) )
4 ishmeo 
 |-  ( ( _I |` X ) e. ( J Homeo J ) <-> ( ( _I |` X ) e. ( J Cn J ) /\ `' ( _I |` X ) e. ( J Cn J ) ) )
5 1 3 4 sylanbrc 
 |-  ( J e. ( TopOn ` X ) -> ( _I |` X ) e. ( J Homeo J ) )