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 \mathrm{TopOn}\left(X\right)\to {\mathrm{I}\upharpoonright }_X\in \left(J\mathrm{Homeo}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		idcn	$$⊢J\in \mathrm{TopOn}\left(X\right)\to {\mathrm{I}\upharpoonright }_X\in \left(J\mathrm{Cn}J\right)$$
2		cnvresid	$$⊢{\left({\mathrm{I}\upharpoonright }_X\right)}^{-1}={\mathrm{I}\upharpoonright }_X$$
3	2 1	eqeltrid	$$⊢J\in \mathrm{TopOn}\left(X\right)\to {\left({\mathrm{I}\upharpoonright }_X\right)}^{-1}\in \left(J\mathrm{Cn}J\right)$$
4		ishmeo	$$⊢{\mathrm{I}\upharpoonright }_X\in \left(J\mathrm{Homeo}J\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_X\in \left(J\mathrm{Cn}J\right)\wedge {\left({\mathrm{I}\upharpoonright }_X\right)}^{-1}\in \left(J\mathrm{Cn}J\right)\right)$$
5	1 3 4	sylanbrc	$$⊢J\in \mathrm{TopOn}\left(X\right)\to {\mathrm{I}\upharpoonright }_X\in \left(J\mathrm{Homeo}J\right)$$