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 ( 𝜑𝐴 ⊆ ℝ )
supadd.a2 ( 𝜑𝐴 ≠ ∅ )
supadd.a3 ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 )
supadd.b1 ( 𝜑𝐵 ⊆ ℝ )
supadd.b2 ( 𝜑𝐵 ≠ ∅ )
supadd.b3 ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 )
supadd.c 𝐶 = { 𝑧 ∣ ∃ 𝑣𝐴𝑏𝐵 𝑧 = ( 𝑣 + 𝑏 ) }
Assertion supadd ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) + sup ( 𝐵 , ℝ , < ) ) = sup ( 𝐶 , ℝ , < ) )

Proof

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