Theorem cnmptid

Description: The identity function is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypothesis	cnmptid.j	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
Assertion	cnmptid	$$⊢\phi \to \left(x\in X⟼x\right)\in \left(J\mathrm{Cn}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnmptid.j	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
2		mptresid	$$⊢{\mathrm{I}\upharpoonright }_X=\left(x\in X⟼x\right)$$
3		idcn	$$⊢J\in \mathrm{TopOn}\left(X\right)\to {\mathrm{I}\upharpoonright }_X\in \left(J\mathrm{Cn}J\right)$$
4	1 3	syl	$$⊢\phi \to {\mathrm{I}\upharpoonright }_X\in \left(J\mathrm{Cn}J\right)$$
5	2 4	eqeltrrid	$$⊢\phi \to \left(x\in X⟼x\right)\in \left(J\mathrm{Cn}J\right)$$