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 bitrid ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑣 + 𝑏 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑤 = ( 𝑎 + 𝑏 ) ) )
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 biimtrid ⊢ ( 𝜑 → ( 𝑤 ∈ 𝐶 → 𝑤 ∈ ℝ ) )
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 biimtrid ⊢ ( 𝜑 → ( 𝑤 ∈ 𝐶 → 𝑤 ≤ ( 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 biimtrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑤 ∈ { 𝑧 ∣ ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 + 𝑏 ) } → 𝑤 ≤ 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 biimtrid ⊢ ( 𝜑 → ( 𝑤 ∈ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( 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 ( 𝐶 , ℝ , < ) )