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

Theorem supadd 11410
Description: The supremum function distributes over addition in a sense similar to that in supmul 11414. (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 11405 . . . . 5 (𝜑 → sup(𝐵, ℝ, < ) ∈ ℝ)
8 eqid 2778 . . . . 5 {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))} = {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}
91, 2, 3, 7, 8supaddc 11409 . . . 4 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}, ℝ, < ))
101sselda 3858 . . . . . . . . . 10 ((𝜑𝑎𝐴) → 𝑎 ∈ ℝ)
1110recnd 10468 . . . . . . . . 9 ((𝜑𝑎𝐴) → 𝑎 ∈ ℂ)
127adantr 473 . . . . . . . . . 10 ((𝜑𝑎𝐴) → sup(𝐵, ℝ, < ) ∈ ℝ)
1312recnd 10468 . . . . . . . . 9 ((𝜑𝑎𝐴) → sup(𝐵, ℝ, < ) ∈ ℂ)
1411, 13addcomd 10642 . . . . . . . 8 ((𝜑𝑎𝐴) → (𝑎 + sup(𝐵, ℝ, < )) = (sup(𝐵, ℝ, < ) + 𝑎))
1514eqeq2d 2788 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑧 = (𝑎 + sup(𝐵, ℝ, < )) ↔ 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)))
1615rexbidva 3241 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < )) ↔ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)))
1716abbidv 2843 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))} = {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)})
1817supeq1d 8705 . . . 4 (𝜑 → sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ))
199, 18eqtrd 2814 . . 3 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ))
20 vex 3418 . . . . . . 7 𝑤 ∈ V
21 eqeq1 2782 . . . . . . . 8 (𝑧 = 𝑤 → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎)))
2221rexbidv 3242 . . . . . . 7 (𝑧 = 𝑤 → (∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ ∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎)))
2320, 22elab 3582 . . . . . 6 (𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ↔ ∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎))
244adantr 473 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → 𝐵 ⊆ ℝ)
255adantr 473 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → 𝐵 ≠ ∅)
266adantr 473 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥)
27 eqid 2778 . . . . . . . . . . 11 {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)} = {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}
2824, 25, 26, 10, 27supaddc 11409 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}, ℝ, < ))
294sselda 3858 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → 𝑏 ∈ ℝ)
3029adantlr 702 . . . . . . . . . . . . . . . 16 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑏 ∈ ℝ)
3130recnd 10468 . . . . . . . . . . . . . . 15 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑏 ∈ ℂ)
3210adantr 473 . . . . . . . . . . . . . . . 16 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑎 ∈ ℝ)
3332recnd 10468 . . . . . . . . . . . . . . 15 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑎 ∈ ℂ)
3431, 33addcomd 10642 . . . . . . . . . . . . . 14 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑏 + 𝑎) = (𝑎 + 𝑏))
3534eqeq2d 2788 . . . . . . . . . . . . 13 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑧 = (𝑏 + 𝑎) ↔ 𝑧 = (𝑎 + 𝑏)))
3635rexbidva 3241 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑧 = (𝑏 + 𝑎) ↔ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)))
3736abbidv 2843 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)} = {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)})
3837supeq1d 8705 . . . . . . . . . 10 ((𝜑𝑎𝐴) → sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}, ℝ, < ) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ))
3928, 38eqtrd 2814 . . . . . . . . 9 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ))
40 eqeq1 2782 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → (𝑧 = (𝑎 + 𝑏) ↔ 𝑤 = (𝑎 + 𝑏)))
4140rexbidv 3242 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (∃𝑏𝐵 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
4220, 41elab 3582 . . . . . . . . . . . 12 (𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ↔ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏))
43 rspe 3249 . . . . . . . . . . . . . . 15 ((𝑎𝐴 ∧ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
44 oveq1 6983 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑎 → (𝑣 + 𝑏) = (𝑎 + 𝑏))
4544eqeq2d 2788 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑎 → (𝑧 = (𝑣 + 𝑏) ↔ 𝑧 = (𝑎 + 𝑏)))
4645rexbidv 3242 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑎 → (∃𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)))
4746cbvrexv 3384 . . . . . . . . . . . . . . . . 17 (∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑧 = (𝑎 + 𝑏))
48402rexbidv 3245 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → (∃𝑎𝐴𝑏𝐵 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
4947, 48syl5bb 275 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → (∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
50 supadd.c . . . . . . . . . . . . . . . 16 𝐶 = {𝑧 ∣ ∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏)}
5120, 49, 50elab2 3585 . . . . . . . . . . . . . . 15 (𝑤𝐶 ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
5243, 51sylibr 226 . . . . . . . . . . . . . 14 ((𝑎𝐴 ∧ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → 𝑤𝐶)
5352ex 405 . . . . . . . . . . . . 13 (𝑎𝐴 → (∃𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤𝐶))
541sseld 3857 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑎𝐴𝑎 ∈ ℝ))
554sseld 3857 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑏𝐵𝑏 ∈ ℝ))
5654, 55anim12d 599 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)))
57 readdcl 10418 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 + 𝑏) ∈ ℝ)
5856, 57syl6 35 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 + 𝑏) ∈ ℝ))
59 eleq1a 2861 . . . . . . . . . . . . . . . . . 18 ((𝑎 + 𝑏) ∈ ℝ → (𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ))
6058, 59syl6 35 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ)))
6160rexlimdvv 3238 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ))
6251, 61syl5bi 234 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤𝐶𝑤 ∈ ℝ))
6362ssrdv 3864 . . . . . . . . . . . . . 14 (𝜑𝐶 ⊆ ℝ)
64 ovex 7008 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 + 𝑏) ∈ V
6564isseti 3429 . . . . . . . . . . . . . . . . . . . . 21 𝑤 𝑤 = (𝑎 + 𝑏)
6665rgenw 3100 . . . . . . . . . . . . . . . . . . . 20 𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏)
67 r19.2z 4323 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ≠ ∅ ∧ ∀𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏)) → ∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏))
685, 66, 67sylancl 577 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏))
69 rexcom4 3196 . . . . . . . . . . . . . . . . . . 19 (∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏) ↔ ∃𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7068, 69sylib 210 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7170ralrimivw 3133 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
72 r19.2z 4323 . . . . . . . . . . . . . . . . 17 ((𝐴 ≠ ∅ ∧ ∀𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → ∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
732, 71, 72syl2anc 576 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
74 rexcom4 3196 . . . . . . . . . . . . . . . 16 (∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏) ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7573, 74sylib 210 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
76 n0 4196 . . . . . . . . . . . . . . . 16 (𝐶 ≠ ∅ ↔ ∃𝑤 𝑤𝐶)
7751exbii 1810 . . . . . . . . . . . . . . . 16 (∃𝑤 𝑤𝐶 ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7876, 77bitri 267 . . . . . . . . . . . . . . 15 (𝐶 ≠ ∅ ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7975, 78sylibr 226 . . . . . . . . . . . . . 14 (𝜑𝐶 ≠ ∅)
801, 2, 3suprcld 11405 . . . . . . . . . . . . . . . 16 (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
8180, 7readdcld 10469 . . . . . . . . . . . . . . 15 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ)
8210adantrr 704 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑎 ∈ ℝ)
8329adantrl 703 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑏 ∈ ℝ)
8480adantr 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → sup(𝐴, ℝ, < ) ∈ ℝ)
857adantr 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → sup(𝐵, ℝ, < ) ∈ ℝ)
861, 2, 33jca 1108 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
87 suprub 11403 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ 𝑎𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
8886, 87sylan 572 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑎𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
8988adantrr 704 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑎 ≤ sup(𝐴, ℝ, < ))
904, 5, 63jca 1108 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥))
91 suprub 11403 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥) ∧ 𝑏𝐵) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9290, 91sylan 572 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9392adantrl 703 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9482, 83, 84, 85, 89, 93le2addd 11060 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
9594ex 405 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
96 breq1 4932 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = (𝑎 + 𝑏) → (𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
9796biimprcd 242 . . . . . . . . . . . . . . . . . . 19 ((𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
9895, 97syl6 35 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))))
9998rexlimdvv 3238 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
10051, 99syl5bi 234 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤𝐶𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
101100ralrimiv 3131 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
102 brralrspcev 4989 . . . . . . . . . . . . . . 15 (((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ ∧ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))) → ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥)
10381, 101, 102syl2anc 576 . . . . . . . . . . . . . 14 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥)
104 suprub 11403 . . . . . . . . . . . . . . 15 (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) ∧ 𝑤𝐶) → 𝑤 ≤ sup(𝐶, ℝ, < ))
105104ex 405 . . . . . . . . . . . . . 14 ((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) → (𝑤𝐶𝑤 ≤ sup(𝐶, ℝ, < )))
10663, 79, 103, 105syl3anc 1351 . . . . . . . . . . . . 13 (𝜑 → (𝑤𝐶𝑤 ≤ sup(𝐶, ℝ, < )))
10753, 106sylan9r 501 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ sup(𝐶, ℝ, < )))
10842, 107syl5bi 234 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → (𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} → 𝑤 ≤ sup(𝐶, ℝ, < )))
109108ralrimiv 3131 . . . . . . . . . 10 ((𝜑𝑎𝐴) → ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < ))
11032, 30readdcld 10469 . . . . . . . . . . . . . 14 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑎 + 𝑏) ∈ ℝ)
111 eleq1a 2861 . . . . . . . . . . . . . 14 ((𝑎 + 𝑏) ∈ ℝ → (𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
112110, 111syl 17 . . . . . . . . . . . . 13 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
113112rexlimdva 3229 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
114113abssdv 3935 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ⊆ ℝ)
11564isseti 3429 . . . . . . . . . . . . . . . 16 𝑧 𝑧 = (𝑎 + 𝑏)
116115rgenw 3100 . . . . . . . . . . . . . . 15 𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏)
117 r19.2z 4323 . . . . . . . . . . . . . . 15 ((𝐵 ≠ ∅ ∧ ∀𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏)) → ∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏))
1185, 116, 117sylancl 577 . . . . . . . . . . . . . 14 (𝜑 → ∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏))
119 rexcom4 3196 . . . . . . . . . . . . . 14 (∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
120118, 119sylib 210 . . . . . . . . . . . . 13 (𝜑 → ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
121 abn0 4222 . . . . . . . . . . . . 13 ({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅ ↔ ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
122120, 121sylibr 226 . . . . . . . . . . . 12 (𝜑 → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅)
123122adantr 473 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅)
12463, 79, 103suprcld 11405 . . . . . . . . . . . . 13 (𝜑 → sup(𝐶, ℝ, < ) ∈ ℝ)
125124adantr 473 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → sup(𝐶, ℝ, < ) ∈ ℝ)
126 brralrspcev 4989 . . . . . . . . . . . 12 ((sup(𝐶, ℝ, < ) ∈ ℝ ∧ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥)
127125, 109, 126syl2anc 576 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥)
128 suprleub 11408 . . . . . . . . . . 11 ((({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥) ∧ sup(𝐶, ℝ, < ) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )))
129114, 123, 127, 125, 128syl31anc 1353 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )))
130109, 129mpbird 249 . . . . . . . . 9 ((𝜑𝑎𝐴) → sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ))
13139, 130eqbrtrd 4951 . . . . . . . 8 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) ≤ sup(𝐶, ℝ, < ))
132 breq1 4932 . . . . . . . 8 (𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → (𝑤 ≤ sup(𝐶, ℝ, < ) ↔ (sup(𝐵, ℝ, < ) + 𝑎) ≤ sup(𝐶, ℝ, < )))
133131, 132syl5ibrcom 239 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑤 ≤ sup(𝐶, ℝ, < )))
134133rexlimdva 3229 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑤 ≤ sup(𝐶, ℝ, < )))
13523, 134syl5bi 234 . . . . 5 (𝜑 → (𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} → 𝑤 ≤ sup(𝐶, ℝ, < )))
136135ralrimiv 3131 . . . 4 (𝜑 → ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < ))
13712, 10readdcld 10469 . . . . . . . 8 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) ∈ ℝ)
138 eleq1a 2861 . . . . . . . 8 ((sup(𝐵, ℝ, < ) + 𝑎) ∈ ℝ → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
139137, 138syl 17 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
140139rexlimdva 3229 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
141140abssdv 3935 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ⊆ ℝ)
142 ovex 7008 . . . . . . . . . 10 (sup(𝐵, ℝ, < ) + 𝑎) ∈ V
143142isseti 3429 . . . . . . . . 9 𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)
144143rgenw 3100 . . . . . . . 8 𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)
145 r19.2z 4323 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)) → ∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
1462, 144, 145sylancl 577 . . . . . . 7 (𝜑 → ∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
147 rexcom4 3196 . . . . . . 7 (∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
148146, 147sylib 210 . . . . . 6 (𝜑 → ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
149 abn0 4222 . . . . . 6 ({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅ ↔ ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
150148, 149sylibr 226 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅)
151 brralrspcev 4989 . . . . . 6 ((sup(𝐶, ℝ, < ) ∈ ℝ ∧ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥)
152124, 136, 151syl2anc 576 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥)
153 suprleub 11408 . . . . 5 ((({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥) ∧ sup(𝐶, ℝ, < ) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )))
154141, 150, 152, 124, 153syl31anc 1353 . . . 4 (𝜑 → (sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )))
155136, 154mpbird 249 . . 3 (𝜑 → sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ))
15619, 155eqbrtrd 4951 . 2 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ≤ sup(𝐶, ℝ, < ))
157 suprleub 11408 . . . 4 (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) ∧ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ) → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
15863, 79, 103, 81, 157syl31anc 1353 . . 3 (𝜑 → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
159101, 158mpbird 249 . 2 (𝜑 → sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
16081, 124letri3d 10582 . 2 (𝜑 → ((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ) ↔ ((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ≤ sup(𝐶, ℝ, < ) ∧ sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))))
161156, 159, 160mpbir2and 700 1 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wex 1742  wcel 2050  {cab 2758  wne 2967  wral 3088  wrex 3089  wss 3829  c0 4178   class class class wbr 4929  (class class class)co 6976  supcsup 8699  cr 10334   + caddc 10338   < clt 10474  cle 10475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412  ax-pre-sup 10413
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-mpt 5009  df-id 5312  df-po 5326  df-so 5327  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-er 8089  df-en 8307  df-dom 8308  df-sdom 8309  df-sup 8701  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673
This theorem is referenced by:  ismblfin  34380  itg2addnc  34393  sge0resplit  42125
  Copyright terms: Public domain W3C validator