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	|- ( ph -> J e. ( TopOn ` X ) )
Assertion	cnmptid	|- ( ph -> ( x e. X |-> x ) e. ( J Cn J ) )

Proof

Step	Hyp	Ref	Expression
1		cnmptid.j	|- ( ph -> J e. ( TopOn ` X ) )
2		mptresid	|- ( _I |` X ) = ( x e. X |-> x )
3		idcn	|- ( J e. ( TopOn ` X ) -> ( _I |` X ) e. ( J Cn J ) )
4	1 3	syl	|- ( ph -> ( _I |` X ) e. ( J Cn J ) )
5	2 4	eqeltrrid	|- ( ph -> ( x e. X |-> x ) e. ( J Cn J ) )