addccncf2

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

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

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

Metamath Proof Explorer