Metamath Proof Explorer


Theorem negcncfg

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

Ref Expression
Hypothesis negcncfg.1 φ x A B : A cn
Assertion negcncfg φ x A B : A cn

Proof

Step Hyp Ref Expression
1 negcncfg.1 φ x A B : A cn
2 df-neg B = 0 B
3 2 a1i φ x A B = 0 B
4 3 mpteq2dva φ x A B = x A 0 B
5 eqid x 0 = x 0
6 0cn 0
7 ssidd 0
8 id 0 0
9 7 8 7 constcncfg 0 x 0 : cn
10 6 9 mp1i φ x 0 : cn
11 cncfrss x A B : A cn A
12 1 11 syl φ A
13 ssidd φ
14 6 a1i φ x A 0
15 5 10 12 13 14 cncfmptssg φ x A 0 : A cn
16 15 1 subcncf φ x A 0 B : A cn
17 4 16 eqeltrd φ x A B : A cn