Metamath Proof Explorer

Theorem supadd

Description: The supremum function distributes over addition in a sense similar to that in supmul . (Contributed by Brendan Leahy, 26-Sep-2017)

Ref Expression
Hypotheses supadd.a1 
|- ( ph -> A C_ RR )
supadd.a2 
|- ( ph -> A =/= (/) )
supadd.a3 
|- ( ph -> E. x e. RR A. y e. A y <_ x )
supadd.b1 
|- ( ph -> B C_ RR )
supadd.b2 
|- ( ph -> B =/= (/) )
supadd.b3 
|- ( ph -> E. x e. RR A. y e. B y <_ x )
supadd.c 
|- C = { z | E. v e. A E. b e. B z = ( v + b ) }
Assertion supadd 
|- ( ph -> ( sup ( A , RR , < ) + sup ( B , RR , < ) ) = sup ( C , RR , < ) )

Proof

Step Hyp Ref Expression
1 supadd.a1 
 |-  ( ph -> A C_ RR )
2 supadd.a2 
 |-  ( ph -> A =/= (/) )
3 supadd.a3 
 |-  ( ph -> E. x e. RR A. y e. A y <_ x )
4 supadd.b1 
 |-  ( ph -> B C_ RR )
5 supadd.b2 
 |-  ( ph -> B =/= (/) )
6 supadd.b3 
 |-  ( ph -> E. x e. RR A. y e. B y <_ x )
7 supadd.c 
 |-  C = { z | E. v e. A E. b e. B z = ( v + b ) }
8 4 5 6 suprcld 
 |-  ( ph -> sup ( B , RR , < ) e. RR )
9 eqid 
 |-  { z | E. a e. A z = ( a + sup ( B , RR , < ) ) } = { z | E. a e. A z = ( a + sup ( B , RR , < ) ) }
10 1 2 3 8 9 supaddc 
 |-  ( ph -> ( sup ( A , RR , < ) + sup ( B , RR , < ) ) = sup ( { z | E. a e. A z = ( a + sup ( B , RR , < ) ) } , RR , < ) )
11 1 sselda 
 |-  ( ( ph /\ a e. A ) -> a e. RR )
12 11 recnd 
 |-  ( ( ph /\ a e. A ) -> a e. CC )
13 8 adantr 
 |-  ( ( ph /\ a e. A ) -> sup ( B , RR , < ) e. RR )
14 13 recnd 
 |-  ( ( ph /\ a e. A ) -> sup ( B , RR , < ) e. CC )
15 12 14 addcomd 
 |-  ( ( ph /\ a e. A ) -> ( a + sup ( B , RR , < ) ) = ( sup ( B , RR , < ) + a ) )
16 15 eqeq2d 
 |-  ( ( ph /\ a e. A ) -> ( z = ( a + sup ( B , RR , < ) ) <-> z = ( sup ( B , RR , < ) + a ) ) )
17 16 rexbidva 
 |-  ( ph -> ( E. a e. A z = ( a + sup ( B , RR , < ) ) <-> E. a e. A z = ( sup ( B , RR , < ) + a ) ) )
18 17 abbidv 
 |-  ( ph -> { z | E. a e. A z = ( a + sup ( B , RR , < ) ) } = { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } )
19 18 supeq1d 
 |-  ( ph -> sup ( { z | E. a e. A z = ( a + sup ( B , RR , < ) ) } , RR , < ) = sup ( { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } , RR , < ) )
20 10 19 eqtrd 
 |-  ( ph -> ( sup ( A , RR , < ) + sup ( B , RR , < ) ) = sup ( { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } , RR , < ) )
21 vex 
 |-  w e. _V
22 eqeq1 
 |-  ( z = w -> ( z = ( sup ( B , RR , < ) + a ) <-> w = ( sup ( B , RR , < ) + a ) ) )
23 22 rexbidv 
 |-  ( z = w -> ( E. a e. A z = ( sup ( B , RR , < ) + a ) <-> E. a e. A w = ( sup ( B , RR , < ) + a ) ) )
24 21 23 elab 
 |-  ( w e. { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } <-> E. a e. A w = ( sup ( B , RR , < ) + a ) )
25 4 adantr 
 |-  ( ( ph /\ a e. A ) -> B C_ RR )
26 5 adantr 
 |-  ( ( ph /\ a e. A ) -> B =/= (/) )
27 6 adantr 
 |-  ( ( ph /\ a e. A ) -> E. x e. RR A. y e. B y <_ x )
28 eqid 
 |-  { z | E. b e. B z = ( b + a ) } = { z | E. b e. B z = ( b + a ) }
29 25 26 27 11 28 supaddc 
 |-  ( ( ph /\ a e. A ) -> ( sup ( B , RR , < ) + a ) = sup ( { z | E. b e. B z = ( b + a ) } , RR , < ) )
30 4 sselda 
 |-  ( ( ph /\ b e. B ) -> b e. RR )
31 30 adantlr 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> b e. RR )
32 31 recnd 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> b e. CC )
33 11 adantr 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> a e. RR )
34 33 recnd 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> a e. CC )
35 32 34 addcomd 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> ( b + a ) = ( a + b ) )
36 35 eqeq2d 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> ( z = ( b + a ) <-> z = ( a + b ) ) )
37 36 rexbidva 
 |-  ( ( ph /\ a e. A ) -> ( E. b e. B z = ( b + a ) <-> E. b e. B z = ( a + b ) ) )
38 37 abbidv 
 |-  ( ( ph /\ a e. A ) -> { z | E. b e. B z = ( b + a ) } = { z | E. b e. B z = ( a + b ) } )
39 38 supeq1d 
 |-  ( ( ph /\ a e. A ) -> sup ( { z | E. b e. B z = ( b + a ) } , RR , < ) = sup ( { z | E. b e. B z = ( a + b ) } , RR , < ) )
40 29 39 eqtrd 
 |-  ( ( ph /\ a e. A ) -> ( sup ( B , RR , < ) + a ) = sup ( { z | E. b e. B z = ( a + b ) } , RR , < ) )
41 eqeq1 
 |-  ( z = w -> ( z = ( a + b ) <-> w = ( a + b ) ) )
42 41 rexbidv 
 |-  ( z = w -> ( E. b e. B z = ( a + b ) <-> E. b e. B w = ( a + b ) ) )
43 21 42 elab 
 |-  ( w e. { z | E. b e. B z = ( a + b ) } <-> E. b e. B w = ( a + b ) )
44 rspe 
 |-  ( ( a e. A /\ E. b e. B w = ( a + b ) ) -> E. a e. A E. b e. B w = ( a + b ) )
45 oveq1 
 |-  ( v = a -> ( v + b ) = ( a + b ) )
46 45 eqeq2d 
 |-  ( v = a -> ( z = ( v + b ) <-> z = ( a + b ) ) )
47 46 rexbidv 
 |-  ( v = a -> ( E. b e. B z = ( v + b ) <-> E. b e. B z = ( a + b ) ) )
48 47 cbvrexvw 
 |-  ( E. v e. A E. b e. B z = ( v + b ) <-> E. a e. A E. b e. B z = ( a + b ) )
49 41 2rexbidv 
 |-  ( z = w -> ( E. a e. A E. b e. B z = ( a + b ) <-> E. a e. A E. b e. B w = ( a + b ) ) )
50 48 49 bitrid 
 |-  ( z = w -> ( E. v e. A E. b e. B z = ( v + b ) <-> E. a e. A E. b e. B w = ( a + b ) ) )
51 21 50 7 elab2 
 |-  ( w e. C <-> E. a e. A E. b e. B w = ( a + b ) )
52 44 51 sylibr 
 |-  ( ( a e. A /\ E. b e. B w = ( a + b ) ) -> w e. C )
53 52 ex 
 |-  ( a e. A -> ( E. b e. B w = ( a + b ) -> w e. C ) )
54 1 sseld 
 |-  ( ph -> ( a e. A -> a e. RR ) )
55 4 sseld 
 |-  ( ph -> ( b e. B -> b e. RR ) )
56 54 55 anim12d 
 |-  ( ph -> ( ( a e. A /\ b e. B ) -> ( a e. RR /\ b e. RR ) ) )
57 readdcl 
 |-  ( ( a e. RR /\ b e. RR ) -> ( a + b ) e. RR )
58 56 57 syl6 
 |-  ( ph -> ( ( a e. A /\ b e. B ) -> ( a + b ) e. RR ) )
59 eleq1a 
 |-  ( ( a + b ) e. RR -> ( w = ( a + b ) -> w e. RR ) )
60 58 59 syl6 
 |-  ( ph -> ( ( a e. A /\ b e. B ) -> ( w = ( a + b ) -> w e. RR ) ) )
61 60 rexlimdvv 
 |-  ( ph -> ( E. a e. A E. b e. B w = ( a + b ) -> w e. RR ) )
62 51 61 biimtrid 
 |-  ( ph -> ( w e. C -> w e. RR ) )
63 62 ssrdv 
 |-  ( ph -> C C_ RR )
64 ovex 
 |-  ( a + b ) e. _V
65 64 isseti 
 |-  E. w w = ( a + b )
66 65 rgenw 
 |-  A. b e. B E. w w = ( a + b )
67 r19.2z 
 |-  ( ( B =/= (/) /\ A. b e. B E. w w = ( a + b ) ) -> E. b e. B E. w w = ( a + b ) )
68 5 66 67 sylancl 
 |-  ( ph -> E. b e. B E. w w = ( a + b ) )
69 rexcom4 
 |-  ( E. b e. B E. w w = ( a + b ) <-> E. w E. b e. B w = ( a + b ) )
70 68 69 sylib 
 |-  ( ph -> E. w E. b e. B w = ( a + b ) )
71 70 ralrimivw 
 |-  ( ph -> A. a e. A E. w E. b e. B w = ( a + b ) )
72 r19.2z 
 |-  ( ( A =/= (/) /\ A. a e. A E. w E. b e. B w = ( a + b ) ) -> E. a e. A E. w E. b e. B w = ( a + b ) )
73 2 71 72 syl2anc 
 |-  ( ph -> E. a e. A E. w E. b e. B w = ( a + b ) )
74 rexcom4 
 |-  ( E. a e. A E. w E. b e. B w = ( a + b ) <-> E. w E. a e. A E. b e. B w = ( a + b ) )
75 73 74 sylib 
 |-  ( ph -> E. w E. a e. A E. b e. B w = ( a + b ) )
76 n0 
 |-  ( C =/= (/) <-> E. w w e. C )
77 51 exbii 
 |-  ( E. w w e. C <-> E. w E. a e. A E. b e. B w = ( a + b ) )
78 76 77 bitri 
 |-  ( C =/= (/) <-> E. w E. a e. A E. b e. B w = ( a + b ) )
79 75 78 sylibr 
 |-  ( ph -> C =/= (/) )
80 1 2 3 suprcld 
 |-  ( ph -> sup ( A , RR , < ) e. RR )
81 80 8 readdcld 
 |-  ( ph -> ( sup ( A , RR , < ) + sup ( B , RR , < ) ) e. RR )
82 11 adantrr 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> a e. RR )
83 30 adantrl 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> b e. RR )
84 80 adantr 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> sup ( A , RR , < ) e. RR )
85 8 adantr 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> sup ( B , RR , < ) e. RR )
86 1 2 3 3jca 
 |-  ( ph -> ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) )
87 suprub 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ a e. A ) -> a <_ sup ( A , RR , < ) )
88 86 87 sylan 
 |-  ( ( ph /\ a e. A ) -> a <_ sup ( A , RR , < ) )
89 88 adantrr 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> a <_ sup ( A , RR , < ) )
90 4 5 6 3jca 
 |-  ( ph -> ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) )
91 suprub 
 |-  ( ( ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) /\ b e. B ) -> b <_ sup ( B , RR , < ) )
92 90 91 sylan 
 |-  ( ( ph /\ b e. B ) -> b <_ sup ( B , RR , < ) )
93 92 adantrl 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> b <_ sup ( B , RR , < ) )
94 82 83 84 85 89 93 le2addd 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> ( a + b ) <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) )
95 94 ex 
 |-  ( ph -> ( ( a e. A /\ b e. B ) -> ( a + b ) <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) ) )
96 breq1 
 |-  ( w = ( a + b ) -> ( w <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) <-> ( a + b ) <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) ) )
97 96 biimprcd 
 |-  ( ( a + b ) <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) -> ( w = ( a + b ) -> w <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) ) )
98 95 97 syl6 
 |-  ( ph -> ( ( a e. A /\ b e. B ) -> ( w = ( a + b ) -> w <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) ) ) )
99 98 rexlimdvv 
 |-  ( ph -> ( E. a e. A E. b e. B w = ( a + b ) -> w <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) ) )
100 51 99 biimtrid 
 |-  ( ph -> ( w e. C -> w <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) ) )
101 100 ralrimiv 
 |-  ( ph -> A. w e. C w <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) )
102 brralrspcev 
 |-  ( ( ( sup ( A , RR , < ) + sup ( B , RR , < ) ) e. RR /\ A. w e. C w <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) ) -> E. x e. RR A. w e. C w <_ x )
103 81 101 102 syl2anc 
 |-  ( ph -> E. x e. RR A. w e. C w <_ x )
104 suprub 
 |-  ( ( ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) /\ w e. C ) -> w <_ sup ( C , RR , < ) )
105 104 ex 
 |-  ( ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) -> ( w e. C -> w <_ sup ( C , RR , < ) ) )
106 63 79 103 105 syl3anc 
 |-  ( ph -> ( w e. C -> w <_ sup ( C , RR , < ) ) )
107 53 106 sylan9r 
 |-  ( ( ph /\ a e. A ) -> ( E. b e. B w = ( a + b ) -> w <_ sup ( C , RR , < ) ) )
108 43 107 biimtrid 
 |-  ( ( ph /\ a e. A ) -> ( w e. { z | E. b e. B z = ( a + b ) } -> w <_ sup ( C , RR , < ) ) )
109 108 ralrimiv 
 |-  ( ( ph /\ a e. A ) -> A. w e. { z | E. b e. B z = ( a + b ) } w <_ sup ( C , RR , < ) )
110 33 31 readdcld 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> ( a + b ) e. RR )
111 eleq1a 
 |-  ( ( a + b ) e. RR -> ( z = ( a + b ) -> z e. RR ) )
112 110 111 syl 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> ( z = ( a + b ) -> z e. RR ) )
113 112 rexlimdva 
 |-  ( ( ph /\ a e. A ) -> ( E. b e. B z = ( a + b ) -> z e. RR ) )
114 113 abssdv 
 |-  ( ( ph /\ a e. A ) -> { z | E. b e. B z = ( a + b ) } C_ RR )
115 64 isseti 
 |-  E. z z = ( a + b )
116 115 rgenw 
 |-  A. b e. B E. z z = ( a + b )
117 r19.2z 
 |-  ( ( B =/= (/) /\ A. b e. B E. z z = ( a + b ) ) -> E. b e. B E. z z = ( a + b ) )
118 5 116 117 sylancl 
 |-  ( ph -> E. b e. B E. z z = ( a + b ) )
119 rexcom4 
 |-  ( E. b e. B E. z z = ( a + b ) <-> E. z E. b e. B z = ( a + b ) )
120 118 119 sylib 
 |-  ( ph -> E. z E. b e. B z = ( a + b ) )
121 abn0 
 |-  ( { z | E. b e. B z = ( a + b ) } =/= (/) <-> E. z E. b e. B z = ( a + b ) )
122 120 121 sylibr 
 |-  ( ph -> { z | E. b e. B z = ( a + b ) } =/= (/) )
123 122 adantr 
 |-  ( ( ph /\ a e. A ) -> { z | E. b e. B z = ( a + b ) } =/= (/) )
124 63 79 103 suprcld 
 |-  ( ph -> sup ( C , RR , < ) e. RR )
125 124 adantr 
 |-  ( ( ph /\ a e. A ) -> sup ( C , RR , < ) e. RR )
126 brralrspcev 
 |-  ( ( sup ( C , RR , < ) e. RR /\ A. w e. { z | E. b e. B z = ( a + b ) } w <_ sup ( C , RR , < ) ) -> E. x e. RR A. w e. { z | E. b e. B z = ( a + b ) } w <_ x )
127 125 109 126 syl2anc 
 |-  ( ( ph /\ a e. A ) -> E. x e. RR A. w e. { z | E. b e. B z = ( a + b ) } w <_ x )
128 suprleub 
 |-  ( ( ( { z | E. b e. B z = ( a + b ) } C_ RR /\ { z | E. b e. B z = ( a + b ) } =/= (/) /\ E. x e. RR A. w e. { z | E. b e. B z = ( a + b ) } w <_ x ) /\ sup ( C , RR , < ) e. RR ) -> ( sup ( { z | E. b e. B z = ( a + b ) } , RR , < ) <_ sup ( C , RR , < ) <-> A. w e. { z | E. b e. B z = ( a + b ) } w <_ sup ( C , RR , < ) ) )
129 114 123 127 125 128 syl31anc 
 |-  ( ( ph /\ a e. A ) -> ( sup ( { z | E. b e. B z = ( a + b ) } , RR , < ) <_ sup ( C , RR , < ) <-> A. w e. { z | E. b e. B z = ( a + b ) } w <_ sup ( C , RR , < ) ) )
130 109 129 mpbird 
 |-  ( ( ph /\ a e. A ) -> sup ( { z | E. b e. B z = ( a + b ) } , RR , < ) <_ sup ( C , RR , < ) )
131 40 130 eqbrtrd 
 |-  ( ( ph /\ a e. A ) -> ( sup ( B , RR , < ) + a ) <_ sup ( C , RR , < ) )
132 breq1 
 |-  ( w = ( sup ( B , RR , < ) + a ) -> ( w <_ sup ( C , RR , < ) <-> ( sup ( B , RR , < ) + a ) <_ sup ( C , RR , < ) ) )
133 131 132 syl5ibrcom 
 |-  ( ( ph /\ a e. A ) -> ( w = ( sup ( B , RR , < ) + a ) -> w <_ sup ( C , RR , < ) ) )
134 133 rexlimdva 
 |-  ( ph -> ( E. a e. A w = ( sup ( B , RR , < ) + a ) -> w <_ sup ( C , RR , < ) ) )
135 24 134 biimtrid 
 |-  ( ph -> ( w e. { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } -> w <_ sup ( C , RR , < ) ) )
136 135 ralrimiv 
 |-  ( ph -> A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } w <_ sup ( C , RR , < ) )
137 13 11 readdcld 
 |-  ( ( ph /\ a e. A ) -> ( sup ( B , RR , < ) + a ) e. RR )
138 eleq1a 
 |-  ( ( sup ( B , RR , < ) + a ) e. RR -> ( z = ( sup ( B , RR , < ) + a ) -> z e. RR ) )
139 137 138 syl 
 |-  ( ( ph /\ a e. A ) -> ( z = ( sup ( B , RR , < ) + a ) -> z e. RR ) )
140 139 rexlimdva 
 |-  ( ph -> ( E. a e. A z = ( sup ( B , RR , < ) + a ) -> z e. RR ) )
141 140 abssdv 
 |-  ( ph -> { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } C_ RR )
142 ovex 
 |-  ( sup ( B , RR , < ) + a ) e. _V
143 142 isseti 
 |-  E. z z = ( sup ( B , RR , < ) + a )
144 143 rgenw 
 |-  A. a e. A E. z z = ( sup ( B , RR , < ) + a )
145 r19.2z 
 |-  ( ( A =/= (/) /\ A. a e. A E. z z = ( sup ( B , RR , < ) + a ) ) -> E. a e. A E. z z = ( sup ( B , RR , < ) + a ) )
146 2 144 145 sylancl 
 |-  ( ph -> E. a e. A E. z z = ( sup ( B , RR , < ) + a ) )
147 rexcom4 
 |-  ( E. a e. A E. z z = ( sup ( B , RR , < ) + a ) <-> E. z E. a e. A z = ( sup ( B , RR , < ) + a ) )
148 146 147 sylib 
 |-  ( ph -> E. z E. a e. A z = ( sup ( B , RR , < ) + a ) )
149 abn0 
 |-  ( { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } =/= (/) <-> E. z E. a e. A z = ( sup ( B , RR , < ) + a ) )
150 148 149 sylibr 
 |-  ( ph -> { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } =/= (/) )
151 brralrspcev 
 |-  ( ( sup ( C , RR , < ) e. RR /\ A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } w <_ sup ( C , RR , < ) ) -> E. x e. RR A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } w <_ x )
152 124 136 151 syl2anc 
 |-  ( ph -> E. x e. RR A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } w <_ x )
153 suprleub 
 |-  ( ( ( { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } C_ RR /\ { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } =/= (/) /\ E. x e. RR A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } w <_ x ) /\ sup ( C , RR , < ) e. RR ) -> ( sup ( { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } , RR , < ) <_ sup ( C , RR , < ) <-> A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } w <_ sup ( C , RR , < ) ) )
154 141 150 152 124 153 syl31anc 
 |-  ( ph -> ( sup ( { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } , RR , < ) <_ sup ( C , RR , < ) <-> A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } w <_ sup ( C , RR , < ) ) )
155 136 154 mpbird 
 |-  ( ph -> sup ( { z | E. a e. A z = ( sup ( B , RR , < ) + a ) } , RR , < ) <_ sup ( C , RR , < ) )
156 20 155 eqbrtrd 
 |-  ( ph -> ( sup ( A , RR , < ) + sup ( B , RR , < ) ) <_ sup ( C , RR , < ) )
157 suprleub 
 |-  ( ( ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) /\ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) e. RR ) -> ( sup ( C , RR , < ) <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) <-> A. w e. C w <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) ) )
158 63 79 103 81 157 syl31anc 
 |-  ( ph -> ( sup ( C , RR , < ) <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) <-> A. w e. C w <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) ) )
159 101 158 mpbird 
 |-  ( ph -> sup ( C , RR , < ) <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) )
160 81 124 letri3d 
 |-  ( ph -> ( ( sup ( A , RR , < ) + sup ( B , RR , < ) ) = sup ( C , RR , < ) <-> ( ( sup ( A , RR , < ) + sup ( B , RR , < ) ) <_ sup ( C , RR , < ) /\ sup ( C , RR , < ) <_ ( sup ( A , RR , < ) + sup ( B , RR , < ) ) ) ) )
161 156 159 160 mpbir2and 
 |-  ( ph -> ( sup ( A , RR , < ) + sup ( B , RR , < ) ) = sup ( C , RR , < ) )