Theorem cncfmptid

Description: The identity function is a continuous function on CC . (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 17-May-2016)

	Ref	Expression
Assertion	cncfmptid	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑥 ∈ 𝑆 ↦ 𝑥 ) ∈ ( 𝑆 –cn→ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		cncfss	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑆 –cn→ 𝑆 ) ⊆ ( 𝑆 –cn→ 𝑇 ) )
2		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3	2	cnfldtopon	⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
4		sstr	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → 𝑆 ⊆ ℂ )
5		resttopon	⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
6	3 4 5	sylancr	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
7	6	cnmptid	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑥 ∈ 𝑆 ↦ 𝑥 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) )
8		eqid	⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
9	2 8 8	cncfcn	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑆 ⊆ ℂ ) → ( 𝑆 –cn→ 𝑆 ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) )
10	4 4 9	syl2anc	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑆 –cn→ 𝑆 ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) )
11	7 10	eleqtrrd	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑥 ∈ 𝑆 ↦ 𝑥 ) ∈ ( 𝑆 –cn→ 𝑆 ) )
12	1 11	sseldd	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑥 ∈ 𝑆 ↦ 𝑥 ) ∈ ( 𝑆 –cn→ 𝑇 ) )