Theorem addccncf2

Description: Adding a constant is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		addccncf2.1	$$⊢F=\left(x\in A⟼B+x\right)$$
2		simpl	$$⊢\left(A\subseteq ℂ\wedge B\in ℂ\right)\to A\subseteq ℂ$$
3		simpr	$$⊢\left(A\subseteq ℂ\wedge B\in ℂ\right)\to B\in ℂ$$
4		ssidd	$$⊢\left(A\subseteq ℂ\wedge B\in ℂ\right)\to ℂ\subseteq ℂ$$
5	2 3 4	constcncfg	$$⊢\left(A\subseteq ℂ\wedge B\in ℂ\right)\to \left(x\in A⟼B\right):A\underset{cn}{⟶}ℂ$$
6		ssid	$$⊢ℂ\subseteq ℂ$$
7		cncfmptid	$$⊢\left(A\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(x\in A⟼x\right):A\underset{cn}{⟶}ℂ$$
8	6 7	mpan2	$$⊢A\subseteq ℂ\to \left(x\in A⟼x\right):A\underset{cn}{⟶}ℂ$$
9	8	adantr	$$⊢\left(A\subseteq ℂ\wedge B\in ℂ\right)\to \left(x\in A⟼x\right):A\underset{cn}{⟶}ℂ$$
10	5 9	addcncf	$$⊢\left(A\subseteq ℂ\wedge B\in ℂ\right)\to \left(x\in A⟼B+x\right):A\underset{cn}{⟶}ℂ$$
11	1 10	eqeltrid	$$⊢\left(A\subseteq ℂ\wedge B\in ℂ\right)\to F:A\underset{cn}{⟶}ℂ$$