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

Theorem supadd 12131
Description: The supremum function distributes over addition in a sense similar to that in supmul 12135. (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 12126 . . . . 5 (𝜑 → sup(𝐵, ℝ, < ) ∈ ℝ)
8 eqid 2733 . . . . 5 {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))} = {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}
91, 2, 3, 7, 8supaddc 12130 . . . 4 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}, ℝ, < ))
101sselda 3948 . . . . . . . . . 10 ((𝜑𝑎𝐴) → 𝑎 ∈ ℝ)
1110recnd 11191 . . . . . . . . 9 ((𝜑𝑎𝐴) → 𝑎 ∈ ℂ)
127adantr 482 . . . . . . . . . 10 ((𝜑𝑎𝐴) → sup(𝐵, ℝ, < ) ∈ ℝ)
1312recnd 11191 . . . . . . . . 9 ((𝜑𝑎𝐴) → sup(𝐵, ℝ, < ) ∈ ℂ)
1411, 13addcomd 11365 . . . . . . . 8 ((𝜑𝑎𝐴) → (𝑎 + sup(𝐵, ℝ, < )) = (sup(𝐵, ℝ, < ) + 𝑎))
1514eqeq2d 2744 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑧 = (𝑎 + sup(𝐵, ℝ, < )) ↔ 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)))
1615rexbidva 3170 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < )) ↔ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)))
1716abbidv 2802 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))} = {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)})
1817supeq1d 9390 . . . 4 (𝜑 → sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ))
199, 18eqtrd 2773 . . 3 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ))
20 vex 3451 . . . . . . 7 𝑤 ∈ V
21 eqeq1 2737 . . . . . . . 8 (𝑧 = 𝑤 → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎)))
2221rexbidv 3172 . . . . . . 7 (𝑧 = 𝑤 → (∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ ∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎)))
2320, 22elab 3634 . . . . . 6 (𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ↔ ∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎))
244adantr 482 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → 𝐵 ⊆ ℝ)
255adantr 482 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → 𝐵 ≠ ∅)
266adantr 482 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥)
27 eqid 2733 . . . . . . . . . . 11 {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)} = {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}
2824, 25, 26, 10, 27supaddc 12130 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}, ℝ, < ))
294sselda 3948 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → 𝑏 ∈ ℝ)
3029adantlr 714 . . . . . . . . . . . . . . . 16 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑏 ∈ ℝ)
3130recnd 11191 . . . . . . . . . . . . . . 15 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑏 ∈ ℂ)
3210adantr 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑎 ∈ ℝ)
3332recnd 11191 . . . . . . . . . . . . . . 15 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑎 ∈ ℂ)
3431, 33addcomd 11365 . . . . . . . . . . . . . 14 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑏 + 𝑎) = (𝑎 + 𝑏))
3534eqeq2d 2744 . . . . . . . . . . . . 13 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑧 = (𝑏 + 𝑎) ↔ 𝑧 = (𝑎 + 𝑏)))
3635rexbidva 3170 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑧 = (𝑏 + 𝑎) ↔ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)))
3736abbidv 2802 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)} = {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)})
3837supeq1d 9390 . . . . . . . . . 10 ((𝜑𝑎𝐴) → sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}, ℝ, < ) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ))
3928, 38eqtrd 2773 . . . . . . . . 9 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ))
40 eqeq1 2737 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → (𝑧 = (𝑎 + 𝑏) ↔ 𝑤 = (𝑎 + 𝑏)))
4140rexbidv 3172 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (∃𝑏𝐵 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
4220, 41elab 3634 . . . . . . . . . . . 12 (𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ↔ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏))
43 rspe 3231 . . . . . . . . . . . . . . 15 ((𝑎𝐴 ∧ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
44 oveq1 7368 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑎 → (𝑣 + 𝑏) = (𝑎 + 𝑏))
4544eqeq2d 2744 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑎 → (𝑧 = (𝑣 + 𝑏) ↔ 𝑧 = (𝑎 + 𝑏)))
4645rexbidv 3172 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑎 → (∃𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)))
4746cbvrexvw 3225 . . . . . . . . . . . . . . . . 17 (∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑧 = (𝑎 + 𝑏))
48402rexbidv 3210 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → (∃𝑎𝐴𝑏𝐵 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
4947, 48bitrid 283 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → (∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
50 supadd.c . . . . . . . . . . . . . . . 16 𝐶 = {𝑧 ∣ ∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏)}
5120, 49, 50elab2 3638 . . . . . . . . . . . . . . 15 (𝑤𝐶 ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
5243, 51sylibr 233 . . . . . . . . . . . . . 14 ((𝑎𝐴 ∧ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → 𝑤𝐶)
5352ex 414 . . . . . . . . . . . . 13 (𝑎𝐴 → (∃𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤𝐶))
541sseld 3947 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑎𝐴𝑎 ∈ ℝ))
554sseld 3947 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑏𝐵𝑏 ∈ ℝ))
5654, 55anim12d 610 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)))
57 readdcl 11142 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 + 𝑏) ∈ ℝ)
5856, 57syl6 35 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 + 𝑏) ∈ ℝ))
59 eleq1a 2829 . . . . . . . . . . . . . . . . . 18 ((𝑎 + 𝑏) ∈ ℝ → (𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ))
6058, 59syl6 35 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ)))
6160rexlimdvv 3201 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ))
6251, 61biimtrid 241 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤𝐶𝑤 ∈ ℝ))
6362ssrdv 3954 . . . . . . . . . . . . . 14 (𝜑𝐶 ⊆ ℝ)
64 ovex 7394 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 + 𝑏) ∈ V
6564isseti 3462 . . . . . . . . . . . . . . . . . . . . 21 𝑤 𝑤 = (𝑎 + 𝑏)
6665rgenw 3065 . . . . . . . . . . . . . . . . . . . 20 𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏)
67 r19.2z 4456 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ≠ ∅ ∧ ∀𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏)) → ∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏))
685, 66, 67sylancl 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏))
69 rexcom4 3270 . . . . . . . . . . . . . . . . . . 19 (∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏) ↔ ∃𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7068, 69sylib 217 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7170ralrimivw 3144 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
72 r19.2z 4456 . . . . . . . . . . . . . . . . 17 ((𝐴 ≠ ∅ ∧ ∀𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → ∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
732, 71, 72syl2anc 585 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
74 rexcom4 3270 . . . . . . . . . . . . . . . 16 (∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏) ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7573, 74sylib 217 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
76 n0 4310 . . . . . . . . . . . . . . . 16 (𝐶 ≠ ∅ ↔ ∃𝑤 𝑤𝐶)
7751exbii 1851 . . . . . . . . . . . . . . . 16 (∃𝑤 𝑤𝐶 ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7876, 77bitri 275 . . . . . . . . . . . . . . 15 (𝐶 ≠ ∅ ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7975, 78sylibr 233 . . . . . . . . . . . . . 14 (𝜑𝐶 ≠ ∅)
801, 2, 3suprcld 12126 . . . . . . . . . . . . . . . 16 (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
8180, 7readdcld 11192 . . . . . . . . . . . . . . 15 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ)
8210adantrr 716 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑎 ∈ ℝ)
8329adantrl 715 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑏 ∈ ℝ)
8480adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → sup(𝐴, ℝ, < ) ∈ ℝ)
857adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → sup(𝐵, ℝ, < ) ∈ ℝ)
861, 2, 33jca 1129 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
87 suprub 12124 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ 𝑎𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
8886, 87sylan 581 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑎𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
8988adantrr 716 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑎 ≤ sup(𝐴, ℝ, < ))
904, 5, 63jca 1129 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥))
91 suprub 12124 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥) ∧ 𝑏𝐵) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9290, 91sylan 581 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9392adantrl 715 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9482, 83, 84, 85, 89, 93le2addd 11782 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
9594ex 414 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
96 breq1 5112 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = (𝑎 + 𝑏) → (𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
9796biimprcd 250 . . . . . . . . . . . . . . . . . . 19 ((𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
9895, 97syl6 35 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))))
9998rexlimdvv 3201 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
10051, 99biimtrid 241 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤𝐶𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
101100ralrimiv 3139 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
102 brralrspcev 5169 . . . . . . . . . . . . . . 15 (((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ ∧ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))) → ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥)
10381, 101, 102syl2anc 585 . . . . . . . . . . . . . 14 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥)
104 suprub 12124 . . . . . . . . . . . . . . 15 (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) ∧ 𝑤𝐶) → 𝑤 ≤ sup(𝐶, ℝ, < ))
105104ex 414 . . . . . . . . . . . . . 14 ((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) → (𝑤𝐶𝑤 ≤ sup(𝐶, ℝ, < )))
10663, 79, 103, 105syl3anc 1372 . . . . . . . . . . . . 13 (𝜑 → (𝑤𝐶𝑤 ≤ sup(𝐶, ℝ, < )))
10753, 106sylan9r 510 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ sup(𝐶, ℝ, < )))
10842, 107biimtrid 241 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → (𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} → 𝑤 ≤ sup(𝐶, ℝ, < )))
109108ralrimiv 3139 . . . . . . . . . 10 ((𝜑𝑎𝐴) → ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < ))
11032, 30readdcld 11192 . . . . . . . . . . . . . 14 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑎 + 𝑏) ∈ ℝ)
111 eleq1a 2829 . . . . . . . . . . . . . 14 ((𝑎 + 𝑏) ∈ ℝ → (𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
112110, 111syl 17 . . . . . . . . . . . . 13 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
113112rexlimdva 3149 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
114113abssdv 4029 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ⊆ ℝ)
11564isseti 3462 . . . . . . . . . . . . . . . 16 𝑧 𝑧 = (𝑎 + 𝑏)
116115rgenw 3065 . . . . . . . . . . . . . . 15 𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏)
117 r19.2z 4456 . . . . . . . . . . . . . . 15 ((𝐵 ≠ ∅ ∧ ∀𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏)) → ∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏))
1185, 116, 117sylancl 587 . . . . . . . . . . . . . 14 (𝜑 → ∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏))
119 rexcom4 3270 . . . . . . . . . . . . . 14 (∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
120118, 119sylib 217 . . . . . . . . . . . . 13 (𝜑 → ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
121 abn0 4344 . . . . . . . . . . . . 13 ({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅ ↔ ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
122120, 121sylibr 233 . . . . . . . . . . . 12 (𝜑 → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅)
123122adantr 482 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅)
12463, 79, 103suprcld 12126 . . . . . . . . . . . . 13 (𝜑 → sup(𝐶, ℝ, < ) ∈ ℝ)
125124adantr 482 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → sup(𝐶, ℝ, < ) ∈ ℝ)
126 brralrspcev 5169 . . . . . . . . . . . 12 ((sup(𝐶, ℝ, < ) ∈ ℝ ∧ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥)
127125, 109, 126syl2anc 585 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥)
128 suprleub 12129 . . . . . . . . . . 11 ((({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥) ∧ sup(𝐶, ℝ, < ) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )))
129114, 123, 127, 125, 128syl31anc 1374 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )))
130109, 129mpbird 257 . . . . . . . . 9 ((𝜑𝑎𝐴) → sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ))
13139, 130eqbrtrd 5131 . . . . . . . 8 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) ≤ sup(𝐶, ℝ, < ))
132 breq1 5112 . . . . . . . 8 (𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → (𝑤 ≤ sup(𝐶, ℝ, < ) ↔ (sup(𝐵, ℝ, < ) + 𝑎) ≤ sup(𝐶, ℝ, < )))
133131, 132syl5ibrcom 247 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑤 ≤ sup(𝐶, ℝ, < )))
134133rexlimdva 3149 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑤 ≤ sup(𝐶, ℝ, < )))
13523, 134biimtrid 241 . . . . 5 (𝜑 → (𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} → 𝑤 ≤ sup(𝐶, ℝ, < )))
136135ralrimiv 3139 . . . 4 (𝜑 → ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < ))
13712, 10readdcld 11192 . . . . . . . 8 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) ∈ ℝ)
138 eleq1a 2829 . . . . . . . 8 ((sup(𝐵, ℝ, < ) + 𝑎) ∈ ℝ → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
139137, 138syl 17 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
140139rexlimdva 3149 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
141140abssdv 4029 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ⊆ ℝ)
142 ovex 7394 . . . . . . . . . 10 (sup(𝐵, ℝ, < ) + 𝑎) ∈ V
143142isseti 3462 . . . . . . . . 9 𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)
144143rgenw 3065 . . . . . . . 8 𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)
145 r19.2z 4456 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)) → ∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
1462, 144, 145sylancl 587 . . . . . . 7 (𝜑 → ∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
147 rexcom4 3270 . . . . . . 7 (∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
148146, 147sylib 217 . . . . . 6 (𝜑 → ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
149 abn0 4344 . . . . . 6 ({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅ ↔ ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
150148, 149sylibr 233 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅)
151 brralrspcev 5169 . . . . . 6 ((sup(𝐶, ℝ, < ) ∈ ℝ ∧ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥)
152124, 136, 151syl2anc 585 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥)
153 suprleub 12129 . . . . 5 ((({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥) ∧ sup(𝐶, ℝ, < ) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )))
154141, 150, 152, 124, 153syl31anc 1374 . . . 4 (𝜑 → (sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )))
155136, 154mpbird 257 . . 3 (𝜑 → sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ))
15619, 155eqbrtrd 5131 . 2 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ≤ sup(𝐶, ℝ, < ))
157 suprleub 12129 . . . 4 (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) ∧ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ) → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
15863, 79, 103, 81, 157syl31anc 1374 . . 3 (𝜑 → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
159101, 158mpbird 257 . 2 (𝜑 → sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
16081, 124letri3d 11305 . 2 (𝜑 → ((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ) ↔ ((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ≤ sup(𝐶, ℝ, < ) ∧ sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))))
161156, 159, 160mpbir2and 712 1 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wex 1782  wcel 2107  {cab 2710  wne 2940  wral 3061  wrex 3070  wss 3914  c0 4286   class class class wbr 5109  (class class class)co 7361  supcsup 9384  cr 11058   + caddc 11062   < clt 11197  cle 11198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-po 5549  df-so 5550  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8654  df-en 8890  df-dom 8891  df-sdom 8892  df-sup 9386  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396
This theorem is referenced by:  ismblfin  36169  itg2addnc  36182  sge0resplit  44737
  Copyright terms: Public domain W3C validator