Theorem sub2cncfd

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

	Ref	Expression
Hypotheses	sub2cncfd.1	$$⊢\phi \to A\in ℂ$$
	sub2cncfd.2	$$⊢F=\left(x\in ℂ⟼A-x\right)$$
Assertion	sub2cncfd	$$⊢\phi \to F:ℂ\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		sub2cncfd.1	$$⊢\phi \to A\in ℂ$$
2		sub2cncfd.2	$$⊢F=\left(x\in ℂ⟼A-x\right)$$
3		ssid	$$⊢ℂ\subseteq ℂ$$
4	3	a1i	$$⊢\phi \to ℂ\subseteq ℂ$$
5		cncfmptc	$$⊢\left(A\in ℂ\wedge ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
6	1 4 4 5	syl3anc	$$⊢\phi \to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
7		cncfmptid	$$⊢\left(ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(x\in ℂ⟼x\right):ℂ\underset{cn}{⟶}ℂ$$
8	3 3 7	mp2an	$$⊢\left(x\in ℂ⟼x\right):ℂ\underset{cn}{⟶}ℂ$$
9	8	a1i	$$⊢\phi \to \left(x\in ℂ⟼x\right):ℂ\underset{cn}{⟶}ℂ$$
10	6 9	subcncf	$$⊢\phi \to \left(x\in ℂ⟼A-x\right):ℂ\underset{cn}{⟶}ℂ$$
11	2 10	eqeltrid	$$⊢\phi \to F:ℂ\underset{cn}{⟶}ℂ$$