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

Metamath Proof Explorer

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	$⊢ φ \to J \in TopOn (X)$
	Assertion	cnmptid	$⊢ φ \to (x \in X ⟼ x) \in (J Cn J)$

Step	Hyp	Ref	Expression
1		cnmptid.j	$⊢ φ \to J \in TopOn (X)$
2		mptresid	$⊢ {I ↾}_{X} = (x \in X ⟼ x)$
3		idcn	$⊢ J \in TopOn (X) \to {I ↾}_{X} \in (J Cn J)$
4	1 3	syl	$⊢ φ \to {I ↾}_{X} \in (J Cn J)$
5	2 4	eqeltrrid	$⊢ φ \to (x \in X ⟼ x) \in (J Cn J)$