# Metamath Proof Explorer

## Theorem cncfmptc

Description: A constant function is a continuous function on CC . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 7-Sep-2015)

Ref Expression
Assertion cncfmptc ${⊢}\left({A}\in {T}\wedge {S}\subseteq ℂ\wedge {T}\subseteq ℂ\right)\to \left({x}\in {S}⟼{A}\right):{S}\underset{cn}{⟶}{T}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 1 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
3 simp2 ${⊢}\left({A}\in {T}\wedge {S}\subseteq ℂ\wedge {T}\subseteq ℂ\right)\to {S}\subseteq ℂ$
4 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)$
5 2 3 4 sylancr ${⊢}\left({A}\in {T}\wedge {S}\subseteq ℂ\wedge {T}\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)$
6 simp3 ${⊢}\left({A}\in {T}\wedge {S}\subseteq ℂ\wedge {T}\subseteq ℂ\right)\to {T}\subseteq ℂ$
7 resttopon ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge {T}\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{T}\in \mathrm{TopOn}\left({T}\right)$
8 2 6 7 sylancr ${⊢}\left({A}\in {T}\wedge {S}\subseteq ℂ\wedge {T}\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{T}\in \mathrm{TopOn}\left({T}\right)$
9 simp1 ${⊢}\left({A}\in {T}\wedge {S}\subseteq ℂ\wedge {T}\subseteq ℂ\right)\to {A}\in {T}$
10 5 8 9 cnmptc ${⊢}\left({A}\in {T}\wedge {S}\subseteq ℂ\wedge {T}\subseteq ℂ\right)\to \left({x}\in {S}⟼{A}\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{T}\right)\right)$
11 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}$
12 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{T}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{T}$
13 1 11 12 cncfcn
15 10 14 eleqtrrd ${⊢}\left({A}\in {T}\wedge {S}\subseteq ℂ\wedge {T}\subseteq ℂ\right)\to \left({x}\in {S}⟼{A}\right):{S}\underset{cn}{⟶}{T}$