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 ) )