Metamath Proof Explorer

Theorem raddcn

Description: Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017)

Ref Expression
Hypothesis raddcn.1 
|- J = ( topGen ` ran (,) )
Assertion raddcn 
|- ( x e. RR , y e. RR |-> ( x + y ) ) e. ( ( J tX J ) Cn J )

Proof

Step Hyp Ref Expression
1 raddcn.1 
 |-  J = ( topGen ` ran (,) )
2 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3 2 addcn 
 |-  + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
4 ax-resscn 
 |-  RR C_ CC
5 xpss12 
 |-  ( ( RR C_ CC /\ RR C_ CC ) -> ( RR X. RR ) C_ ( CC X. CC ) )
6 4 4 5 mp2an 
 |-  ( RR X. RR ) C_ ( CC X. CC )
7 2 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
8 2 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
9 8 toponunii 
 |-  CC = U. ( TopOpen ` CCfld )
10 7 7 9 9 txunii 
 |-  ( CC X. CC ) = U. ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) )
11 10 cnrest 
 |-  ( ( + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) /\ ( RR X. RR ) C_ ( CC X. CC ) ) -> ( + |` ( RR X. RR ) ) e. ( ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) |`t ( RR X. RR ) ) Cn ( TopOpen ` CCfld ) ) )
12 3 6 11 mp2an 
 |-  ( + |` ( RR X. RR ) ) e. ( ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) |`t ( RR X. RR ) ) Cn ( TopOpen ` CCfld ) )
13 reex 
 |-  RR e. _V
14 txrest 
 |-  ( ( ( ( TopOpen ` CCfld ) e. Top /\ ( TopOpen ` CCfld ) e. Top ) /\ ( RR e. _V /\ RR e. _V ) ) -> ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) |`t ( RR X. RR ) ) = ( ( ( TopOpen ` CCfld ) |`t RR ) tX ( ( TopOpen ` CCfld ) |`t RR ) ) )
15 7 7 13 13 14 mp4an 
 |-  ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) |`t ( RR X. RR ) ) = ( ( ( TopOpen ` CCfld ) |`t RR ) tX ( ( TopOpen ` CCfld ) |`t RR ) )
16 2 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
17 1 16 eqtr2i 
 |-  ( ( TopOpen ` CCfld ) |`t RR ) = J
18 17 17 oveq12i 
 |-  ( ( ( TopOpen ` CCfld ) |`t RR ) tX ( ( TopOpen ` CCfld ) |`t RR ) ) = ( J tX J )
19 15 18 eqtri 
 |-  ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) |`t ( RR X. RR ) ) = ( J tX J )
20 19 oveq1i 
 |-  ( ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) |`t ( RR X. RR ) ) Cn ( TopOpen ` CCfld ) ) = ( ( J tX J ) Cn ( TopOpen ` CCfld ) )
21 12 20 eleqtri 
 |-  ( + |` ( RR X. RR ) ) e. ( ( J tX J ) Cn ( TopOpen ` CCfld ) )
22 ax-addf 
 |-  + : ( CC X. CC ) --> CC
23 ffn 
 |-  ( + : ( CC X. CC ) --> CC -> + Fn ( CC X. CC ) )
24 22 23 ax-mp 
 |-  + Fn ( CC X. CC )
25 fnssres 
 |-  ( ( + Fn ( CC X. CC ) /\ ( RR X. RR ) C_ ( CC X. CC ) ) -> ( + |` ( RR X. RR ) ) Fn ( RR X. RR ) )
26 24 6 25 mp2an 
 |-  ( + |` ( RR X. RR ) ) Fn ( RR X. RR )
27 fnov 
 |-  ( ( + |` ( RR X. RR ) ) Fn ( RR X. RR ) <-> ( + |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> ( x ( + |` ( RR X. RR ) ) y ) ) )
28 26 27 mpbi 
 |-  ( + |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> ( x ( + |` ( RR X. RR ) ) y ) )
29 ovres 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x ( + |` ( RR X. RR ) ) y ) = ( x + y ) )
30 29 mpoeq3ia 
 |-  ( x e. RR , y e. RR |-> ( x ( + |` ( RR X. RR ) ) y ) ) = ( x e. RR , y e. RR |-> ( x + y ) )
31 28 30 eqtri 
 |-  ( + |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> ( x + y ) )
32 31 rneqi 
 |-  ran ( + |` ( RR X. RR ) ) = ran ( x e. RR , y e. RR |-> ( x + y ) )
33 readdcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
34 33 rgen2 
 |-  A. x e. RR A. y e. RR ( x + y ) e. RR
35 eqid 
 |-  ( x e. RR , y e. RR |-> ( x + y ) ) = ( x e. RR , y e. RR |-> ( x + y ) )
36 35 rnmposs 
 |-  ( A. x e. RR A. y e. RR ( x + y ) e. RR -> ran ( x e. RR , y e. RR |-> ( x + y ) ) C_ RR )
37 34 36 ax-mp 
 |-  ran ( x e. RR , y e. RR |-> ( x + y ) ) C_ RR
38 32 37 eqsstri 
 |-  ran ( + |` ( RR X. RR ) ) C_ RR
39 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( + |` ( RR X. RR ) ) C_ RR /\ RR C_ CC ) -> ( ( + |` ( RR X. RR ) ) e. ( ( J tX J ) Cn ( TopOpen ` CCfld ) ) <-> ( + |` ( RR X. RR ) ) e. ( ( J tX J ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
40 8 38 4 39 mp3an 
 |-  ( ( + |` ( RR X. RR ) ) e. ( ( J tX J ) Cn ( TopOpen ` CCfld ) ) <-> ( + |` ( RR X. RR ) ) e. ( ( J tX J ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
41 21 40 mpbi 
 |-  ( + |` ( RR X. RR ) ) e. ( ( J tX J ) Cn ( ( TopOpen ` CCfld ) |`t RR ) )
42 17 oveq2i 
 |-  ( ( J tX J ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) = ( ( J tX J ) Cn J )
43 41 31 42 3eltr3i 
 |-  ( x e. RR , y e. RR |-> ( x + y ) ) e. ( ( J tX J ) Cn J )