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 -1x=-x$$
4	3	mpteq2dva	$$⊢A\subseteq ℂ\to \left(x\in A⟼-1x\right)=\left(x\in A⟼-x\right)$$
5	4 1	eqtr4di	$$⊢A\subseteq ℂ\to \left(x\in A⟼-1x\right)=F$$
6		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
7	6	mulcn	$$⊢\times \in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
8	7	a1i	$$⊢A\subseteq ℂ\to \times \in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_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⟼-1x\right):A\underset{cn}{⟶}ℂ$$
16	5 15	eqeltrrd	$$⊢A\subseteq ℂ\to F:A\underset{cn}{⟶}ℂ$$