negcncfg

Description: The opposite of a continuous function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Hypothesis	negcncfg.1	$⊢ φ \to (x \in A ⟼ B) : A \underset{cn}{⟶} ℂ$
	Assertion	negcncfg	$⊢ φ \to (x \in A ⟼ - B) : A \underset{cn}{⟶} ℂ$

Step	Hyp	Ref	Expression
1		negcncfg.1	$⊢ φ \to (x \in A ⟼ B) : A \underset{cn}{⟶} ℂ$
2		df-neg	$⊢ - B = 0 - B$
3	2	a1i	$⊢ (φ \land x \in A) \to - B = 0 - B$
4	3	mpteq2dva	$⊢ φ \to (x \in A ⟼ - B) = (x \in A ⟼ 0 - B)$
5		eqid	$⊢ (x \in ℂ ⟼ 0) = (x \in ℂ ⟼ 0)$
6		0cn	$⊢ 0 \in ℂ$
7		ssidd	$⊢ 0 \in ℂ \to ℂ \subseteq ℂ$
8		id	$⊢ 0 \in ℂ \to 0 \in ℂ$
9	7 8 7	constcncfg	$⊢ 0 \in ℂ \to (x \in ℂ ⟼ 0) : ℂ \underset{cn}{⟶} ℂ$
10	6 9	mp1i	$⊢ φ \to (x \in ℂ ⟼ 0) : ℂ \underset{cn}{⟶} ℂ$
11		cncfrss	$⊢ (x \in A ⟼ B) : A \underset{cn}{⟶} ℂ \to A \subseteq ℂ$
12	1 11	syl	$⊢ φ \to A \subseteq ℂ$
13		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
14	6	a1i	$⊢ (φ \land x \in A) \to 0 \in ℂ$
15	5 10 12 13 14	cncfmptssg	$⊢ φ \to (x \in A ⟼ 0) : A \underset{cn}{⟶} ℂ$
16	15 1	subcncf	$⊢ φ \to (x \in A ⟼ 0 - B) : A \underset{cn}{⟶} ℂ$
17	4 16	eqeltrd	$⊢ φ \to (x \in A ⟼ - B) : A \underset{cn}{⟶} ℂ$

Metamath Proof Explorer