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	⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ 𝑥 )
	Assertion	idcncf	⊢ 𝐹 ∈ ( ℂ –cn→ ℂ )

Proof

Step	Hyp	Ref	Expression
1		idcncf.1	⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ 𝑥 )
2		ssid	⊢ ℂ ⊆ ℂ
3		cncfmptid	⊢ ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ℂ –cn→ ℂ ) )
4	2 2 3	mp2an	⊢ ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ℂ –cn→ ℂ )
5	1 4	eqeltri	⊢ 𝐹 ∈ ( ℂ –cn→ ℂ )