This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in TopOn (X) \to {I ↾}_{X} \in (J Homeo J)$

Step	Hyp	Ref	Expression
1		idcn	$⊢ J \in TopOn (X) \to {I ↾}_{X} \in (J Cn J)$
2		cnvresid	$⊢ {({I ↾}_{X})}^{-1} = {I ↾}_{X}$
3	2 1	eqeltrid	$⊢ J \in TopOn (X) \to {({I ↾}_{X})}^{-1} \in (J Cn J)$
4		ishmeo	$⊢ {I ↾}_{X} \in (J Homeo J) \leftrightarrow ({I ↾}_{X} \in (J Cn J) \land {({I ↾}_{X})}^{-1} \in (J Cn J))$
5	1 3 4	sylanbrc	$⊢ J \in TopOn (X) \to {I ↾}_{X} \in (J Homeo J)$