Theorem add1cncf

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

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

Proof

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