This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrofsup

Description: The supremum is preserved by extended addition set operation. (Provided minus infinity is not involved as it does not behave well with addition.) (Contributed by Thierry Arnoux, 20-Mar-2017)

Ref Expression
Hypotheses xrofsup.1 
|- ( ph -> X C_ RR* )
xrofsup.2 
|- ( ph -> Y C_ RR* )
xrofsup.3 
|- ( ph -> sup ( X , RR* , < ) =/= -oo )
xrofsup.4 
|- ( ph -> sup ( Y , RR* , < ) =/= -oo )
xrofsup.5 
|- ( ph -> Z = ( +e " ( X X. Y ) ) )
Assertion xrofsup 
|- ( ph -> sup ( Z , RR* , < ) = ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )

Proof

Step Hyp Ref Expression
1 xrofsup.1 
 |-  ( ph -> X C_ RR* )
2 xrofsup.2 
 |-  ( ph -> Y C_ RR* )
3 xrofsup.3 
 |-  ( ph -> sup ( X , RR* , < ) =/= -oo )
4 xrofsup.4 
 |-  ( ph -> sup ( Y , RR* , < ) =/= -oo )
5 xrofsup.5 
 |-  ( ph -> Z = ( +e " ( X X. Y ) ) )
6 1 sseld 
 |-  ( ph -> ( x e. X -> x e. RR* ) )
7 2 sseld 
 |-  ( ph -> ( y e. Y -> y e. RR* ) )
8 6 7 anim12d 
 |-  ( ph -> ( ( x e. X /\ y e. Y ) -> ( x e. RR* /\ y e. RR* ) ) )
9 8 imp 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( x e. RR* /\ y e. RR* ) )
10 xaddcl 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x +e y ) e. RR* )
11 9 10 syl 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( x +e y ) e. RR* )
12 11 ralrimivva 
 |-  ( ph -> A. x e. X A. y e. Y ( x +e y ) e. RR* )
13 fveq2 
 |-  ( u = <. x , y >. -> ( +e ` u ) = ( +e ` <. x , y >. ) )
14 df-ov 
 |-  ( x +e y ) = ( +e ` <. x , y >. )
15 13 14 eqtr4di 
 |-  ( u = <. x , y >. -> ( +e ` u ) = ( x +e y ) )
16 15 eleq1d 
 |-  ( u = <. x , y >. -> ( ( +e ` u ) e. RR* <-> ( x +e y ) e. RR* ) )
17 16 ralxp 
 |-  ( A. u e. ( X X. Y ) ( +e ` u ) e. RR* <-> A. x e. X A. y e. Y ( x +e y ) e. RR* )
18 12 17 sylibr 
 |-  ( ph -> A. u e. ( X X. Y ) ( +e ` u ) e. RR* )
19 xaddf 
 |-  +e : ( RR* X. RR* ) --> RR*
20 ffun 
 |-  ( +e : ( RR* X. RR* ) --> RR* -> Fun +e )
21 19 20 ax-mp 
 |-  Fun +e
22 xpss12 
 |-  ( ( X C_ RR* /\ Y C_ RR* ) -> ( X X. Y ) C_ ( RR* X. RR* ) )
23 1 2 22 syl2anc 
 |-  ( ph -> ( X X. Y ) C_ ( RR* X. RR* ) )
24 19 fdmi 
 |-  dom +e = ( RR* X. RR* )
25 23 24 sseqtrrdi 
 |-  ( ph -> ( X X. Y ) C_ dom +e )
26 funimass4 
 |-  ( ( Fun +e /\ ( X X. Y ) C_ dom +e ) -> ( ( +e " ( X X. Y ) ) C_ RR* <-> A. u e. ( X X. Y ) ( +e ` u ) e. RR* ) )
27 21 25 26 sylancr 
 |-  ( ph -> ( ( +e " ( X X. Y ) ) C_ RR* <-> A. u e. ( X X. Y ) ( +e ` u ) e. RR* ) )
28 18 27 mpbird 
 |-  ( ph -> ( +e " ( X X. Y ) ) C_ RR* )
29 5 28 eqsstrd 
 |-  ( ph -> Z C_ RR* )
30 supxrcl 
 |-  ( X C_ RR* -> sup ( X , RR* , < ) e. RR* )
31 1 30 syl 
 |-  ( ph -> sup ( X , RR* , < ) e. RR* )
32 supxrcl 
 |-  ( Y C_ RR* -> sup ( Y , RR* , < ) e. RR* )
33 2 32 syl 
 |-  ( ph -> sup ( Y , RR* , < ) e. RR* )
34 31 33 xaddcld 
 |-  ( ph -> ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) e. RR* )
35 5 eleq2d 
 |-  ( ph -> ( z e. Z <-> z e. ( +e " ( X X. Y ) ) ) )
36 35 pm5.32i 
 |-  ( ( ph /\ z e. Z ) <-> ( ph /\ z e. ( +e " ( X X. Y ) ) ) )
37 nfvd 
 |-  ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) -> F/ x z <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )
38 nfvd 
 |-  ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) -> F/ y z <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )
39 1 ad2antrr 
 |-  ( ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) /\ ( x e. X /\ y e. Y ) ) -> X C_ RR* )
40 simprl 
 |-  ( ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) /\ ( x e. X /\ y e. Y ) ) -> x e. X )
41 supxrub 
 |-  ( ( X C_ RR* /\ x e. X ) -> x <_ sup ( X , RR* , < ) )
42 39 40 41 syl2anc 
 |-  ( ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) /\ ( x e. X /\ y e. Y ) ) -> x <_ sup ( X , RR* , < ) )
43 2 ad2antrr 
 |-  ( ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) /\ ( x e. X /\ y e. Y ) ) -> Y C_ RR* )
44 simprr 
 |-  ( ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) /\ ( x e. X /\ y e. Y ) ) -> y e. Y )
45 supxrub 
 |-  ( ( Y C_ RR* /\ y e. Y ) -> y <_ sup ( Y , RR* , < ) )
46 43 44 45 syl2anc 
 |-  ( ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) /\ ( x e. X /\ y e. Y ) ) -> y <_ sup ( Y , RR* , < ) )
47 39 40 sseldd 
 |-  ( ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) /\ ( x e. X /\ y e. Y ) ) -> x e. RR* )
48 43 44 sseldd 
 |-  ( ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) /\ ( x e. X /\ y e. Y ) ) -> y e. RR* )
49 39 30 syl 
 |-  ( ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) /\ ( x e. X /\ y e. Y ) ) -> sup ( X , RR* , < ) e. RR* )
50 43 32 syl 
 |-  ( ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) /\ ( x e. X /\ y e. Y ) ) -> sup ( Y , RR* , < ) e. RR* )
51 xle2add 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ ( sup ( X , RR* , < ) e. RR* /\ sup ( Y , RR* , < ) e. RR* ) ) -> ( ( x <_ sup ( X , RR* , < ) /\ y <_ sup ( Y , RR* , < ) ) -> ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) )
52 47 48 49 50 51 syl22anc 
 |-  ( ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) /\ ( x e. X /\ y e. Y ) ) -> ( ( x <_ sup ( X , RR* , < ) /\ y <_ sup ( Y , RR* , < ) ) -> ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) )
53 42 46 52 mp2and 
 |-  ( ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) /\ ( x e. X /\ y e. Y ) ) -> ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )
54 53 ralrimivva 
 |-  ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) -> A. x e. X A. y e. Y ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )
55 fvelima 
 |-  ( ( Fun +e /\ z e. ( +e " ( X X. Y ) ) ) -> E. u e. ( X X. Y ) ( +e ` u ) = z )
56 21 55 mpan 
 |-  ( z e. ( +e " ( X X. Y ) ) -> E. u e. ( X X. Y ) ( +e ` u ) = z )
57 56 adantl 
 |-  ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) -> E. u e. ( X X. Y ) ( +e ` u ) = z )
58 15 eqeq1d 
 |-  ( u = <. x , y >. -> ( ( +e ` u ) = z <-> ( x +e y ) = z ) )
59 58 rexxp 
 |-  ( E. u e. ( X X. Y ) ( +e ` u ) = z <-> E. x e. X E. y e. Y ( x +e y ) = z )
60 57 59 sylib 
 |-  ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) -> E. x e. X E. y e. Y ( x +e y ) = z )
61 54 60 r19.29d2r 
 |-  ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) -> E. x e. X E. y e. Y ( ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) /\ ( x +e y ) = z ) )
62 ancom 
 |-  ( ( ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) /\ ( x +e y ) = z ) <-> ( ( x +e y ) = z /\ ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) )
63 62 2rexbii 
 |-  ( E. x e. X E. y e. Y ( ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) /\ ( x +e y ) = z ) <-> E. x e. X E. y e. Y ( ( x +e y ) = z /\ ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) )
64 61 63 sylib 
 |-  ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) -> E. x e. X E. y e. Y ( ( x +e y ) = z /\ ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) )
65 breq1 
 |-  ( ( x +e y ) = z -> ( ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) <-> z <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) )
66 65 biimpa 
 |-  ( ( ( x +e y ) = z /\ ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> z <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )
67 66 reximi 
 |-  ( E. y e. Y ( ( x +e y ) = z /\ ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> E. y e. Y z <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )
68 67 reximi 
 |-  ( E. x e. X E. y e. Y ( ( x +e y ) = z /\ ( x +e y ) <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> E. x e. X E. y e. Y z <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )
69 64 68 syl 
 |-  ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) -> E. x e. X E. y e. Y z <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )
70 37 38 69 19.9d2r 
 |-  ( ( ph /\ z e. ( +e " ( X X. Y ) ) ) -> z <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )
71 36 70 sylbi 
 |-  ( ( ph /\ z e. Z ) -> z <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )
72 71 ralrimiva 
 |-  ( ph -> A. z e. Z z <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )
73 1 ad2antrr 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> X C_ RR* )
74 2 ad2antrr 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> Y C_ RR* )
75 simplr 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> z e. RR )
76 31 ad2antrr 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> sup ( X , RR* , < ) e. RR* )
77 33 ad2antrr 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> sup ( Y , RR* , < ) e. RR* )
78 3 ad2antrr 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> sup ( X , RR* , < ) =/= -oo )
79 4 ad2antrr 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> sup ( Y , RR* , < ) =/= -oo )
80 simpr 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )
81 75 76 77 78 79 80 xlt2addrd 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> E. a e. RR* E. b e. RR* ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) )
82 nfv 
 |-  F/ b ( X C_ RR* /\ Y C_ RR* )
83 nfcv 
 |-  F/_ b RR*
84 nfre1 
 |-  F/ b E. b e. RR* ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) )
85 83 84 nfrexw 
 |-  F/ b E. a e. RR* E. b e. RR* ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) )
86 82 85 nfan 
 |-  F/ b ( ( X C_ RR* /\ Y C_ RR* ) /\ E. a e. RR* E. b e. RR* ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) )
87 nfvd 
 |-  ( ( ( X C_ RR* /\ Y C_ RR* ) /\ E. a e. RR* E. b e. RR* ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) -> F/ a E. v e. X E. w e. Y z < ( v +e w ) )
88 nfvd 
 |-  ( ( ( X C_ RR* /\ Y C_ RR* ) /\ E. a e. RR* E. b e. RR* ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) -> F/ b E. v e. X E. w e. Y z < ( v +e w ) )
89 id 
 |-  ( ( X C_ RR* /\ Y C_ RR* ) -> ( X C_ RR* /\ Y C_ RR* ) )
90 89 ralrimivw 
 |-  ( ( X C_ RR* /\ Y C_ RR* ) -> A. b e. RR* ( X C_ RR* /\ Y C_ RR* ) )
91 90 ralrimivw 
 |-  ( ( X C_ RR* /\ Y C_ RR* ) -> A. a e. RR* A. b e. RR* ( X C_ RR* /\ Y C_ RR* ) )
92 91 adantr 
 |-  ( ( ( X C_ RR* /\ Y C_ RR* ) /\ E. a e. RR* E. b e. RR* ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) -> A. a e. RR* A. b e. RR* ( X C_ RR* /\ Y C_ RR* ) )
93 simpr 
 |-  ( ( ( X C_ RR* /\ Y C_ RR* ) /\ E. a e. RR* E. b e. RR* ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) -> E. a e. RR* E. b e. RR* ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) )
94 92 93 r19.29d2r 
 |-  ( ( ( X C_ RR* /\ Y C_ RR* ) /\ E. a e. RR* E. b e. RR* ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) -> E. a e. RR* E. b e. RR* ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) )
95 simplrr 
 |-  ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ ( v e. X /\ w e. Y /\ ( a < v /\ b < w ) ) ) -> ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) )
96 95 3anassrs 
 |-  ( ( ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ v e. X ) /\ w e. Y ) /\ ( a < v /\ b < w ) ) -> ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) )
97 96 simp1d 
 |-  ( ( ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ v e. X ) /\ w e. Y ) /\ ( a < v /\ b < w ) ) -> z = ( a +e b ) )
98 simp-4l 
 |-  ( ( ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ v e. X ) /\ w e. Y ) /\ ( a < v /\ b < w ) ) -> ( a e. RR* /\ b e. RR* ) )
99 simplrl 
 |-  ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ ( v e. X /\ w e. Y /\ ( a < v /\ b < w ) ) ) -> ( X C_ RR* /\ Y C_ RR* ) )
100 99 3anassrs 
 |-  ( ( ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ v e. X ) /\ w e. Y ) /\ ( a < v /\ b < w ) ) -> ( X C_ RR* /\ Y C_ RR* ) )
101 100 simpld 
 |-  ( ( ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ v e. X ) /\ w e. Y ) /\ ( a < v /\ b < w ) ) -> X C_ RR* )
102 simpllr 
 |-  ( ( ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ v e. X ) /\ w e. Y ) /\ ( a < v /\ b < w ) ) -> v e. X )
103 101 102 sseldd 
 |-  ( ( ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ v e. X ) /\ w e. Y ) /\ ( a < v /\ b < w ) ) -> v e. RR* )
104 100 simprd 
 |-  ( ( ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ v e. X ) /\ w e. Y ) /\ ( a < v /\ b < w ) ) -> Y C_ RR* )
105 simplr 
 |-  ( ( ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ v e. X ) /\ w e. Y ) /\ ( a < v /\ b < w ) ) -> w e. Y )
106 104 105 sseldd 
 |-  ( ( ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ v e. X ) /\ w e. Y ) /\ ( a < v /\ b < w ) ) -> w e. RR* )
107 98 103 106 jca32 
 |-  ( ( ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ v e. X ) /\ w e. Y ) /\ ( a < v /\ b < w ) ) -> ( ( a e. RR* /\ b e. RR* ) /\ ( v e. RR* /\ w e. RR* ) ) )
108 simpr 
 |-  ( ( ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ v e. X ) /\ w e. Y ) /\ ( a < v /\ b < w ) ) -> ( a < v /\ b < w ) )
109 xlt2add 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ ( v e. RR* /\ w e. RR* ) ) -> ( ( a < v /\ b < w ) -> ( a +e b ) < ( v +e w ) ) )
110 109 imp 
 |-  ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( v e. RR* /\ w e. RR* ) ) /\ ( a < v /\ b < w ) ) -> ( a +e b ) < ( v +e w ) )
111 breq1 
 |-  ( z = ( a +e b ) -> ( z < ( v +e w ) <-> ( a +e b ) < ( v +e w ) ) )
112 111 biimpar 
 |-  ( ( z = ( a +e b ) /\ ( a +e b ) < ( v +e w ) ) -> z < ( v +e w ) )
113 110 112 sylan2 
 |-  ( ( z = ( a +e b ) /\ ( ( ( a e. RR* /\ b e. RR* ) /\ ( v e. RR* /\ w e. RR* ) ) /\ ( a < v /\ b < w ) ) ) -> z < ( v +e w ) )
114 97 107 108 113 syl12anc 
 |-  ( ( ( ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) /\ v e. X ) /\ w e. Y ) /\ ( a < v /\ b < w ) ) -> z < ( v +e w ) )
115 simplll 
 |-  ( ( ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) /\ ( a e. RR* /\ b e. RR* ) ) -> X C_ RR* )
116 simprl 
 |-  ( ( ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) /\ ( a e. RR* /\ b e. RR* ) ) -> a e. RR* )
117 simplr2 
 |-  ( ( ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) /\ ( a e. RR* /\ b e. RR* ) ) -> a < sup ( X , RR* , < ) )
118 supxrlub 
 |-  ( ( X C_ RR* /\ a e. RR* ) -> ( a < sup ( X , RR* , < ) <-> E. v e. X a < v ) )
119 118 biimpa 
 |-  ( ( ( X C_ RR* /\ a e. RR* ) /\ a < sup ( X , RR* , < ) ) -> E. v e. X a < v )
120 115 116 117 119 syl21anc 
 |-  ( ( ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) /\ ( a e. RR* /\ b e. RR* ) ) -> E. v e. X a < v )
121 simpllr 
 |-  ( ( ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) /\ ( a e. RR* /\ b e. RR* ) ) -> Y C_ RR* )
122 simprr 
 |-  ( ( ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) /\ ( a e. RR* /\ b e. RR* ) ) -> b e. RR* )
123 simplr3 
 |-  ( ( ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) /\ ( a e. RR* /\ b e. RR* ) ) -> b < sup ( Y , RR* , < ) )
124 supxrlub 
 |-  ( ( Y C_ RR* /\ b e. RR* ) -> ( b < sup ( Y , RR* , < ) <-> E. w e. Y b < w ) )
125 124 biimpa 
 |-  ( ( ( Y C_ RR* /\ b e. RR* ) /\ b < sup ( Y , RR* , < ) ) -> E. w e. Y b < w )
126 121 122 123 125 syl21anc 
 |-  ( ( ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) /\ ( a e. RR* /\ b e. RR* ) ) -> E. w e. Y b < w )
127 reeanv 
 |-  ( E. v e. X E. w e. Y ( a < v /\ b < w ) <-> ( E. v e. X a < v /\ E. w e. Y b < w ) )
128 120 126 127 sylanbrc 
 |-  ( ( ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) /\ ( a e. RR* /\ b e. RR* ) ) -> E. v e. X E. w e. Y ( a < v /\ b < w ) )
129 128 ancoms 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) -> E. v e. X E. w e. Y ( a < v /\ b < w ) )
130 114 129 reximddv2 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) ) -> E. v e. X E. w e. Y z < ( v +e w ) )
131 130 ex 
 |-  ( ( a e. RR* /\ b e. RR* ) -> ( ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) -> E. v e. X E. w e. Y z < ( v +e w ) ) )
132 131 reximdva 
 |-  ( a e. RR* -> ( E. b e. RR* ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) -> E. b e. RR* E. v e. X E. w e. Y z < ( v +e w ) ) )
133 132 reximia 
 |-  ( E. a e. RR* E. b e. RR* ( ( X C_ RR* /\ Y C_ RR* ) /\ ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) -> E. a e. RR* E. b e. RR* E. v e. X E. w e. Y z < ( v +e w ) )
134 94 133 syl 
 |-  ( ( ( X C_ RR* /\ Y C_ RR* ) /\ E. a e. RR* E. b e. RR* ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) -> E. a e. RR* E. b e. RR* E. v e. X E. w e. Y z < ( v +e w ) )
135 86 87 88 134 19.9d2rf 
 |-  ( ( ( X C_ RR* /\ Y C_ RR* ) /\ E. a e. RR* E. b e. RR* ( z = ( a +e b ) /\ a < sup ( X , RR* , < ) /\ b < sup ( Y , RR* , < ) ) ) -> E. v e. X E. w e. Y z < ( v +e w ) )
136 73 74 81 135 syl21anc 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> E. v e. X E. w e. Y z < ( v +e w ) )
137 simprl 
 |-  ( ( ph /\ ( v e. X /\ w e. Y ) ) -> v e. X )
138 simprr 
 |-  ( ( ph /\ ( v e. X /\ w e. Y ) ) -> w e. Y )
139 21 a1i 
 |-  ( ( ph /\ ( v e. X /\ w e. Y ) ) -> Fun +e )
140 25 adantr 
 |-  ( ( ph /\ ( v e. X /\ w e. Y ) ) -> ( X X. Y ) C_ dom +e )
141 137 138 139 140 elovimad 
 |-  ( ( ph /\ ( v e. X /\ w e. Y ) ) -> ( v +e w ) e. ( +e " ( X X. Y ) ) )
142 5 eleq2d 
 |-  ( ph -> ( ( v +e w ) e. Z <-> ( v +e w ) e. ( +e " ( X X. Y ) ) ) )
143 142 adantr 
 |-  ( ( ph /\ ( v e. X /\ w e. Y ) ) -> ( ( v +e w ) e. Z <-> ( v +e w ) e. ( +e " ( X X. Y ) ) ) )
144 141 143 mpbird 
 |-  ( ( ph /\ ( v e. X /\ w e. Y ) ) -> ( v +e w ) e. Z )
145 simpr 
 |-  ( ( ( ph /\ ( v e. X /\ w e. Y ) ) /\ k = ( v +e w ) ) -> k = ( v +e w ) )
146 145 breq2d 
 |-  ( ( ( ph /\ ( v e. X /\ w e. Y ) ) /\ k = ( v +e w ) ) -> ( z < k <-> z < ( v +e w ) ) )
147 144 146 rspcedv 
 |-  ( ( ph /\ ( v e. X /\ w e. Y ) ) -> ( z < ( v +e w ) -> E. k e. Z z < k ) )
148 147 rexlimdvva 
 |-  ( ph -> ( E. v e. X E. w e. Y z < ( v +e w ) -> E. k e. Z z < k ) )
149 148 ad2antrr 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> ( E. v e. X E. w e. Y z < ( v +e w ) -> E. k e. Z z < k ) )
150 136 149 mpd 
 |-  ( ( ( ph /\ z e. RR ) /\ z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) ) -> E. k e. Z z < k )
151 150 ex 
 |-  ( ( ph /\ z e. RR ) -> ( z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) -> E. k e. Z z < k ) )
152 151 ralrimiva 
 |-  ( ph -> A. z e. RR ( z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) -> E. k e. Z z < k ) )
153 supxr2 
 |-  ( ( ( Z C_ RR* /\ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) e. RR* ) /\ ( A. z e. Z z <_ ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) /\ A. z e. RR ( z < ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) -> E. k e. Z z < k ) ) ) -> sup ( Z , RR* , < ) = ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )
154 29 34 72 152 153 syl22anc 
 |-  ( ph -> sup ( Z , RR* , < ) = ( sup ( X , RR* , < ) +e sup ( Y , RR* , < ) ) )