Theorem addccncf

Description: Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		addccncf.1	$$⊢F=\left(x\in ℂ⟼x+A\right)$$
2		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
3	2	addcn	$$⊢+\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)$$
4	3	a1i	$$⊢A\in ℂ\to +\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)$$
5		ssid	$$⊢ℂ\subseteq ℂ$$
6		cncfmptid	$$⊢\left(ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(x\in ℂ⟼x\right):ℂ\underset{cn}{⟶}ℂ$$
7	5 5 6	mp2an	$$⊢\left(x\in ℂ⟼x\right):ℂ\underset{cn}{⟶}ℂ$$
8	7	a1i	$$⊢A\in ℂ\to \left(x\in ℂ⟼x\right):ℂ\underset{cn}{⟶}ℂ$$
9		cncfmptc	$$⊢\left(A\in ℂ\wedge ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
10	5 5 9	mp3an23	$$⊢A\in ℂ\to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
11	2 4 8 10	cncfmpt2f	$$⊢A\in ℂ\to \left(x\in ℂ⟼x+A\right):ℂ\underset{cn}{⟶}ℂ$$
12	1 11	eqeltrid	$$⊢A\in ℂ\to F:ℂ\underset{cn}{⟶}ℂ$$