# Metamath Proof Explorer

## Theorem negcncf

Description: The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypothesis negcncf.1 ${⊢}{F}=\left({x}\in {A}⟼-{x}\right)$
Assertion negcncf ${⊢}{A}\subseteq ℂ\to {F}:{A}\underset{cn}{⟶}ℂ$

### Proof

Step Hyp Ref Expression
1 negcncf.1 ${⊢}{F}=\left({x}\in {A}⟼-{x}\right)$
2 ssel2 ${⊢}\left({A}\subseteq ℂ\wedge {x}\in {A}\right)\to {x}\in ℂ$
3 2 mulm1d ${⊢}\left({A}\subseteq ℂ\wedge {x}\in {A}\right)\to -1{x}=-{x}$
4 3 mpteq2dva ${⊢}{A}\subseteq ℂ\to \left({x}\in {A}⟼-1{x}\right)=\left({x}\in {A}⟼-{x}\right)$
5 4 1 eqtr4di ${⊢}{A}\subseteq ℂ\to \left({x}\in {A}⟼-1{x}\right)={F}$
6 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
7 6 mulcn ${⊢}×\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
8 7 a1i ${⊢}{A}\subseteq ℂ\to ×\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
9 neg1cn ${⊢}-1\in ℂ$
10 ssid ${⊢}ℂ\subseteq ℂ$
11 cncfmptc ${⊢}\left(-1\in ℂ\wedge {A}\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left({x}\in {A}⟼-1\right):{A}\underset{cn}{⟶}ℂ$
12 9 10 11 mp3an13 ${⊢}{A}\subseteq ℂ\to \left({x}\in {A}⟼-1\right):{A}\underset{cn}{⟶}ℂ$
13 cncfmptid ${⊢}\left({A}\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left({x}\in {A}⟼{x}\right):{A}\underset{cn}{⟶}ℂ$
14 10 13 mpan2 ${⊢}{A}\subseteq ℂ\to \left({x}\in {A}⟼{x}\right):{A}\underset{cn}{⟶}ℂ$
15 6 8 12 14 cncfmpt2f ${⊢}{A}\subseteq ℂ\to \left({x}\in {A}⟼-1{x}\right):{A}\underset{cn}{⟶}ℂ$
16 5 15 eqeltrrd ${⊢}{A}\subseteq ℂ\to {F}:{A}\underset{cn}{⟶}ℂ$