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=\left(x\in ℂ⟼x\right)$$
Assertion	idcncf	$$⊢F:ℂ\underset{cn}{⟶}ℂ$$

Proof

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