Theorem add2cncf

Description: Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	add2cncf.a	$$⊢\phi \to A\in ℂ$$
	add2cncf.f	$$⊢F=\left(x\in ℂ⟼A+x\right)$$
Assertion	add2cncf	$$⊢\phi \to F:ℂ\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		add2cncf.a	$$⊢\phi \to A\in ℂ$$
2		add2cncf.f	$$⊢F=\left(x\in ℂ⟼A+x\right)$$
3		ssid	$$⊢ℂ\subseteq ℂ$$
4	3	a1i	$$⊢A\in ℂ\to ℂ\subseteq ℂ$$
5		cncfmptc	$$⊢\left(A\in ℂ\wedge ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
6	4 4 5	mpd3an23	$$⊢A\in ℂ\to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
7	1 6	syl	$$⊢\phi \to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
8		cncfmptid	$$⊢\left(ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(x\in ℂ⟼x\right):ℂ\underset{cn}{⟶}ℂ$$
9	3 3 8	mp2an	$$⊢\left(x\in ℂ⟼x\right):ℂ\underset{cn}{⟶}ℂ$$
10	9	a1i	$$⊢\phi \to \left(x\in ℂ⟼x\right):ℂ\underset{cn}{⟶}ℂ$$
11	7 10	addcncf	$$⊢\phi \to \left(x\in ℂ⟼A+x\right):ℂ\underset{cn}{⟶}ℂ$$
12	2 11	eqeltrid	$$⊢\phi \to F:ℂ\underset{cn}{⟶}ℂ$$