MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  supadd Structured version   Visualization version   GIF version

Theorem supadd 12234
Description: The supremum function distributes over addition in a sense similar to that in supmul 12238. (Contributed by Brendan Leahy, 26-Sep-2017.)
Hypotheses
Ref Expression
supadd.a1 (𝜑𝐴 ⊆ ℝ)
supadd.a2 (𝜑𝐴 ≠ ∅)
supadd.a3 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)
supadd.b1 (𝜑𝐵 ⊆ ℝ)
supadd.b2 (𝜑𝐵 ≠ ∅)
supadd.b3 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥)
supadd.c 𝐶 = {𝑧 ∣ ∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏)}
Assertion
Ref Expression
supadd (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑏,𝑣,𝐴   𝑥,𝐵,𝑦,𝑧,𝑏,𝑣   𝑥,𝐶   𝜑,𝑧,𝑏,𝑣
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐶(𝑦,𝑧,𝑣,𝑏)

Proof of Theorem supadd
Dummy variables 𝑤 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 supadd.a1 . . . . 5 (𝜑𝐴 ⊆ ℝ)
2 supadd.a2 . . . . 5 (𝜑𝐴 ≠ ∅)
3 supadd.a3 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)
4 supadd.b1 . . . . . 6 (𝜑𝐵 ⊆ ℝ)
5 supadd.b2 . . . . . 6 (𝜑𝐵 ≠ ∅)
6 supadd.b3 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥)
74, 5, 6suprcld 12229 . . . . 5 (𝜑 → sup(𝐵, ℝ, < ) ∈ ℝ)
8 eqid 2726 . . . . 5 {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))} = {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}
91, 2, 3, 7, 8supaddc 12233 . . . 4 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}, ℝ, < ))
101sselda 3979 . . . . . . . . . 10 ((𝜑𝑎𝐴) → 𝑎 ∈ ℝ)
1110recnd 11292 . . . . . . . . 9 ((𝜑𝑎𝐴) → 𝑎 ∈ ℂ)
127adantr 479 . . . . . . . . . 10 ((𝜑𝑎𝐴) → sup(𝐵, ℝ, < ) ∈ ℝ)
1312recnd 11292 . . . . . . . . 9 ((𝜑𝑎𝐴) → sup(𝐵, ℝ, < ) ∈ ℂ)
1411, 13addcomd 11466 . . . . . . . 8 ((𝜑𝑎𝐴) → (𝑎 + sup(𝐵, ℝ, < )) = (sup(𝐵, ℝ, < ) + 𝑎))
1514eqeq2d 2737 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑧 = (𝑎 + sup(𝐵, ℝ, < )) ↔ 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)))
1615rexbidva 3167 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < )) ↔ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)))
1716abbidv 2795 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))} = {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)})
1817supeq1d 9489 . . . 4 (𝜑 → sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ))
199, 18eqtrd 2766 . . 3 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ))
20 vex 3466 . . . . . . 7 𝑤 ∈ V
21 eqeq1 2730 . . . . . . . 8 (𝑧 = 𝑤 → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎)))
2221rexbidv 3169 . . . . . . 7 (𝑧 = 𝑤 → (∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ ∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎)))
2320, 22elab 3666 . . . . . 6 (𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ↔ ∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎))
244adantr 479 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → 𝐵 ⊆ ℝ)
255adantr 479 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → 𝐵 ≠ ∅)
266adantr 479 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥)
27 eqid 2726 . . . . . . . . . . 11 {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)} = {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}
2824, 25, 26, 10, 27supaddc 12233 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}, ℝ, < ))
294sselda 3979 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → 𝑏 ∈ ℝ)
3029adantlr 713 . . . . . . . . . . . . . . . 16 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑏 ∈ ℝ)
3130recnd 11292 . . . . . . . . . . . . . . 15 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑏 ∈ ℂ)
3210adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑎 ∈ ℝ)
3332recnd 11292 . . . . . . . . . . . . . . 15 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑎 ∈ ℂ)
3431, 33addcomd 11466 . . . . . . . . . . . . . 14 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑏 + 𝑎) = (𝑎 + 𝑏))
3534eqeq2d 2737 . . . . . . . . . . . . 13 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑧 = (𝑏 + 𝑎) ↔ 𝑧 = (𝑎 + 𝑏)))
3635rexbidva 3167 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑧 = (𝑏 + 𝑎) ↔ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)))
3736abbidv 2795 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)} = {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)})
3837supeq1d 9489 . . . . . . . . . 10 ((𝜑𝑎𝐴) → sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}, ℝ, < ) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ))
3928, 38eqtrd 2766 . . . . . . . . 9 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ))
40 eqeq1 2730 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → (𝑧 = (𝑎 + 𝑏) ↔ 𝑤 = (𝑎 + 𝑏)))
4140rexbidv 3169 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (∃𝑏𝐵 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
4220, 41elab 3666 . . . . . . . . . . . 12 (𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ↔ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏))
43 rspe 3237 . . . . . . . . . . . . . . 15 ((𝑎𝐴 ∧ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
44 oveq1 7431 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑎 → (𝑣 + 𝑏) = (𝑎 + 𝑏))
4544eqeq2d 2737 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑎 → (𝑧 = (𝑣 + 𝑏) ↔ 𝑧 = (𝑎 + 𝑏)))
4645rexbidv 3169 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑎 → (∃𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)))
4746cbvrexvw 3226 . . . . . . . . . . . . . . . . 17 (∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑧 = (𝑎 + 𝑏))
48402rexbidv 3210 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → (∃𝑎𝐴𝑏𝐵 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
4947, 48bitrid 282 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → (∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
50 supadd.c . . . . . . . . . . . . . . . 16 𝐶 = {𝑧 ∣ ∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏)}
5120, 49, 50elab2 3670 . . . . . . . . . . . . . . 15 (𝑤𝐶 ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
5243, 51sylibr 233 . . . . . . . . . . . . . 14 ((𝑎𝐴 ∧ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → 𝑤𝐶)
5352ex 411 . . . . . . . . . . . . 13 (𝑎𝐴 → (∃𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤𝐶))
541sseld 3978 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑎𝐴𝑎 ∈ ℝ))
554sseld 3978 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑏𝐵𝑏 ∈ ℝ))
5654, 55anim12d 607 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)))
57 readdcl 11241 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 + 𝑏) ∈ ℝ)
5856, 57syl6 35 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 + 𝑏) ∈ ℝ))
59 eleq1a 2821 . . . . . . . . . . . . . . . . . 18 ((𝑎 + 𝑏) ∈ ℝ → (𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ))
6058, 59syl6 35 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ)))
6160rexlimdvv 3201 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ))
6251, 61biimtrid 241 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤𝐶𝑤 ∈ ℝ))
6362ssrdv 3985 . . . . . . . . . . . . . 14 (𝜑𝐶 ⊆ ℝ)
64 ovex 7457 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 + 𝑏) ∈ V
6564isseti 3479 . . . . . . . . . . . . . . . . . . . . 21 𝑤 𝑤 = (𝑎 + 𝑏)
6665rgenw 3055 . . . . . . . . . . . . . . . . . . . 20 𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏)
67 r19.2z 4499 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ≠ ∅ ∧ ∀𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏)) → ∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏))
685, 66, 67sylancl 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏))
69 rexcom4 3276 . . . . . . . . . . . . . . . . . . 19 (∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏) ↔ ∃𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7068, 69sylib 217 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7170ralrimivw 3140 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
72 r19.2z 4499 . . . . . . . . . . . . . . . . 17 ((𝐴 ≠ ∅ ∧ ∀𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → ∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
732, 71, 72syl2anc 582 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
74 rexcom4 3276 . . . . . . . . . . . . . . . 16 (∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏) ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7573, 74sylib 217 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
76 n0 4349 . . . . . . . . . . . . . . . 16 (𝐶 ≠ ∅ ↔ ∃𝑤 𝑤𝐶)
7751exbii 1843 . . . . . . . . . . . . . . . 16 (∃𝑤 𝑤𝐶 ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7876, 77bitri 274 . . . . . . . . . . . . . . 15 (𝐶 ≠ ∅ ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7975, 78sylibr 233 . . . . . . . . . . . . . 14 (𝜑𝐶 ≠ ∅)
801, 2, 3suprcld 12229 . . . . . . . . . . . . . . . 16 (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
8180, 7readdcld 11293 . . . . . . . . . . . . . . 15 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ)
8210adantrr 715 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑎 ∈ ℝ)
8329adantrl 714 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑏 ∈ ℝ)
8480adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → sup(𝐴, ℝ, < ) ∈ ℝ)
857adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → sup(𝐵, ℝ, < ) ∈ ℝ)
861, 2, 33jca 1125 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
87 suprub 12227 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ 𝑎𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
8886, 87sylan 578 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑎𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
8988adantrr 715 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑎 ≤ sup(𝐴, ℝ, < ))
904, 5, 63jca 1125 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥))
91 suprub 12227 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥) ∧ 𝑏𝐵) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9290, 91sylan 578 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9392adantrl 714 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9482, 83, 84, 85, 89, 93le2addd 11883 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
9594ex 411 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
96 breq1 5156 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = (𝑎 + 𝑏) → (𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
9796biimprcd 249 . . . . . . . . . . . . . . . . . . 19 ((𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
9895, 97syl6 35 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))))
9998rexlimdvv 3201 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
10051, 99biimtrid 241 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤𝐶𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
101100ralrimiv 3135 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
102 brralrspcev 5213 . . . . . . . . . . . . . . 15 (((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ ∧ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))) → ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥)
10381, 101, 102syl2anc 582 . . . . . . . . . . . . . 14 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥)
104 suprub 12227 . . . . . . . . . . . . . . 15 (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) ∧ 𝑤𝐶) → 𝑤 ≤ sup(𝐶, ℝ, < ))
105104ex 411 . . . . . . . . . . . . . 14 ((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) → (𝑤𝐶𝑤 ≤ sup(𝐶, ℝ, < )))
10663, 79, 103, 105syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → (𝑤𝐶𝑤 ≤ sup(𝐶, ℝ, < )))
10753, 106sylan9r 507 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ sup(𝐶, ℝ, < )))
10842, 107biimtrid 241 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → (𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} → 𝑤 ≤ sup(𝐶, ℝ, < )))
109108ralrimiv 3135 . . . . . . . . . 10 ((𝜑𝑎𝐴) → ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < ))
11032, 30readdcld 11293 . . . . . . . . . . . . . 14 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑎 + 𝑏) ∈ ℝ)
111 eleq1a 2821 . . . . . . . . . . . . . 14 ((𝑎 + 𝑏) ∈ ℝ → (𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
112110, 111syl 17 . . . . . . . . . . . . 13 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
113112rexlimdva 3145 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
114113abssdv 4064 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ⊆ ℝ)
11564isseti 3479 . . . . . . . . . . . . . . . 16 𝑧 𝑧 = (𝑎 + 𝑏)
116115rgenw 3055 . . . . . . . . . . . . . . 15 𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏)
117 r19.2z 4499 . . . . . . . . . . . . . . 15 ((𝐵 ≠ ∅ ∧ ∀𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏)) → ∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏))
1185, 116, 117sylancl 584 . . . . . . . . . . . . . 14 (𝜑 → ∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏))
119 rexcom4 3276 . . . . . . . . . . . . . 14 (∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
120118, 119sylib 217 . . . . . . . . . . . . 13 (𝜑 → ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
121 abn0 4385 . . . . . . . . . . . . 13 ({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅ ↔ ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
122120, 121sylibr 233 . . . . . . . . . . . 12 (𝜑 → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅)
123122adantr 479 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅)
12463, 79, 103suprcld 12229 . . . . . . . . . . . . 13 (𝜑 → sup(𝐶, ℝ, < ) ∈ ℝ)
125124adantr 479 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → sup(𝐶, ℝ, < ) ∈ ℝ)
126 brralrspcev 5213 . . . . . . . . . . . 12 ((sup(𝐶, ℝ, < ) ∈ ℝ ∧ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥)
127125, 109, 126syl2anc 582 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥)
128 suprleub 12232 . . . . . . . . . . 11 ((({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥) ∧ sup(𝐶, ℝ, < ) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )))
129114, 123, 127, 125, 128syl31anc 1370 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )))
130109, 129mpbird 256 . . . . . . . . 9 ((𝜑𝑎𝐴) → sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ))
13139, 130eqbrtrd 5175 . . . . . . . 8 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) ≤ sup(𝐶, ℝ, < ))
132 breq1 5156 . . . . . . . 8 (𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → (𝑤 ≤ sup(𝐶, ℝ, < ) ↔ (sup(𝐵, ℝ, < ) + 𝑎) ≤ sup(𝐶, ℝ, < )))
133131, 132syl5ibrcom 246 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑤 ≤ sup(𝐶, ℝ, < )))
134133rexlimdva 3145 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑤 ≤ sup(𝐶, ℝ, < )))
13523, 134biimtrid 241 . . . . 5 (𝜑 → (𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} → 𝑤 ≤ sup(𝐶, ℝ, < )))
136135ralrimiv 3135 . . . 4 (𝜑 → ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < ))
13712, 10readdcld 11293 . . . . . . . 8 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) ∈ ℝ)
138 eleq1a 2821 . . . . . . . 8 ((sup(𝐵, ℝ, < ) + 𝑎) ∈ ℝ → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
139137, 138syl 17 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
140139rexlimdva 3145 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
141140abssdv 4064 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ⊆ ℝ)
142 ovex 7457 . . . . . . . . . 10 (sup(𝐵, ℝ, < ) + 𝑎) ∈ V
143142isseti 3479 . . . . . . . . 9 𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)
144143rgenw 3055 . . . . . . . 8 𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)
145 r19.2z 4499 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)) → ∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
1462, 144, 145sylancl 584 . . . . . . 7 (𝜑 → ∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
147 rexcom4 3276 . . . . . . 7 (∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
148146, 147sylib 217 . . . . . 6 (𝜑 → ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
149 abn0 4385 . . . . . 6 ({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅ ↔ ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
150148, 149sylibr 233 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅)
151 brralrspcev 5213 . . . . . 6 ((sup(𝐶, ℝ, < ) ∈ ℝ ∧ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥)
152124, 136, 151syl2anc 582 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥)
153 suprleub 12232 . . . . 5 ((({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥) ∧ sup(𝐶, ℝ, < ) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )))
154141, 150, 152, 124, 153syl31anc 1370 . . . 4 (𝜑 → (sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )))
155136, 154mpbird 256 . . 3 (𝜑 → sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ))
15619, 155eqbrtrd 5175 . 2 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ≤ sup(𝐶, ℝ, < ))
157 suprleub 12232 . . . 4 (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) ∧ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ) → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
15863, 79, 103, 81, 157syl31anc 1370 . . 3 (𝜑 → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
159101, 158mpbird 256 . 2 (𝜑 → sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
16081, 124letri3d 11406 . 2 (𝜑 → ((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ) ↔ ((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ≤ sup(𝐶, ℝ, < ) ∧ sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))))
161156, 159, 160mpbir2and 711 1 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wex 1774  wcel 2099  {cab 2703  wne 2930  wral 3051  wrex 3060  wss 3947  c0 4325   class class class wbr 5153  (class class class)co 7424  supcsup 9483  cr 11157   + caddc 11161   < clt 11298  cle 11299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235  ax-pre-sup 11236
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-po 5594  df-so 5595  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-er 8734  df-en 8975  df-dom 8976  df-sdom 8977  df-sup 9485  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497
This theorem is referenced by:  ismblfin  37362  itg2addnc  37375  sge0resplit  46027
  Copyright terms: Public domain W3C validator