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

Metamath Proof Explorer

Theorem idcncf

Description: The identity function is a continuous function on CC . (Contributed by Jeff Madsen, 11-Jun-2010) (Moved into main set.mm as cncfmptid and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015)

		Ref	Expression
	Hypothesis	idcncf.1	$⊢ F = (x \in ℂ ⟼ x)$
	Assertion	idcncf	$⊢ F : ℂ \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		idcncf.1	$⊢ F = (x \in ℂ ⟼ x)$
2		ssid	$⊢ ℂ \subseteq ℂ$
3		cncfmptid	$⊢ (ℂ \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in ℂ ⟼ x) : ℂ \underset{cn}{⟶} ℂ$
4	2 2 3	mp2an	$⊢ (x \in ℂ ⟼ x) : ℂ \underset{cn}{⟶} ℂ$
5	1 4	eqeltri	$⊢ F : ℂ \underset{cn}{⟶} ℂ$