# Metamath Proof Explorer

## 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 ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to \left({x}\in {S}⟼{x}\right):{S}\underset{cn}{⟶}{T}$

### Proof

Step Hyp Ref Expression
1 cncfss
2 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
3 2 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
4 sstr ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to {S}\subseteq ℂ$
5 resttopon ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge {S}\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)$
6 3 4 5 sylancr ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)$
7 6 cnmptid ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to \left({x}\in {S}⟼{x}\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\right)$
8 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}$
9 2 8 8 cncfcn
10 4 4 9 syl2anc
11 7 10 eleqtrrd ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to \left({x}\in {S}⟼{x}\right):{S}\underset{cn}{⟶}{S}$
12 1 11 sseldd ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to \left({x}\in {S}⟼{x}\right):{S}\underset{cn}{⟶}{T}$