Metamath Proof Explorer


Theorem negcncf

Description: The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypothesis negcncf.1
|- F = ( x e. A |-> -u x )
Assertion negcncf
|- ( A C_ CC -> F e. ( A -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 negcncf.1
 |-  F = ( x e. A |-> -u x )
2 ssel2
 |-  ( ( A C_ CC /\ x e. A ) -> x e. CC )
3 2 mulm1d
 |-  ( ( A C_ CC /\ x e. A ) -> ( -u 1 x. x ) = -u x )
4 3 mpteq2dva
 |-  ( A C_ CC -> ( x e. A |-> ( -u 1 x. x ) ) = ( x e. A |-> -u x ) )
5 4 1 eqtr4di
 |-  ( A C_ CC -> ( x e. A |-> ( -u 1 x. x ) ) = F )
6 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
7 6 mulcn
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
8 7 a1i
 |-  ( A C_ CC -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
9 neg1cn
 |-  -u 1 e. CC
10 ssid
 |-  CC C_ CC
11 cncfmptc
 |-  ( ( -u 1 e. CC /\ A C_ CC /\ CC C_ CC ) -> ( x e. A |-> -u 1 ) e. ( A -cn-> CC ) )
12 9 10 11 mp3an13
 |-  ( A C_ CC -> ( x e. A |-> -u 1 ) e. ( A -cn-> CC ) )
13 cncfmptid
 |-  ( ( A C_ CC /\ CC C_ CC ) -> ( x e. A |-> x ) e. ( A -cn-> CC ) )
14 10 13 mpan2
 |-  ( A C_ CC -> ( x e. A |-> x ) e. ( A -cn-> CC ) )
15 6 8 12 14 cncfmpt2f
 |-  ( A C_ CC -> ( x e. A |-> ( -u 1 x. x ) ) e. ( A -cn-> CC ) )
16 5 15 eqeltrrd
 |-  ( A C_ CC -> F e. ( A -cn-> CC ) )