Theorem idcn

Description: A restricted identity function is a continuous function. (Contributed by FL, 27-Dec-2006) (Proof shortened by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	idcn	$$⊢J\in \mathrm{TopOn}\left(X\right)\to {\mathrm{I}\upharpoonright }_X\in \left(J\mathrm{Cn}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢J\subseteq J$$
2		ssidcn	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge J\in \mathrm{TopOn}\left(X\right)\right)\to \left({\mathrm{I}\upharpoonright }_X\in \left(J\mathrm{Cn}J\right)\leftrightarrow J\subseteq J\right)$$
3	2	anidms	$$⊢J\in \mathrm{TopOn}\left(X\right)\to \left({\mathrm{I}\upharpoonright }_X\in \left(J\mathrm{Cn}J\right)\leftrightarrow J\subseteq J\right)$$
4	1 3	mpbiri	$$⊢J\in \mathrm{TopOn}\left(X\right)\to {\mathrm{I}\upharpoonright }_X\in \left(J\mathrm{Cn}J\right)$$