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

Theorem supadd 12036
Description: The supremum function distributes over addition in a sense similar to that in supmul 12040. (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 12031 . . . . 5 (𝜑 → sup(𝐵, ℝ, < ) ∈ ℝ)
8 eqid 2736 . . . . 5 {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))} = {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}
91, 2, 3, 7, 8supaddc 12035 . . . 4 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}, ℝ, < ))
101sselda 3931 . . . . . . . . . 10 ((𝜑𝑎𝐴) → 𝑎 ∈ ℝ)
1110recnd 11096 . . . . . . . . 9 ((𝜑𝑎𝐴) → 𝑎 ∈ ℂ)
127adantr 481 . . . . . . . . . 10 ((𝜑𝑎𝐴) → sup(𝐵, ℝ, < ) ∈ ℝ)
1312recnd 11096 . . . . . . . . 9 ((𝜑𝑎𝐴) → sup(𝐵, ℝ, < ) ∈ ℂ)
1411, 13addcomd 11270 . . . . . . . 8 ((𝜑𝑎𝐴) → (𝑎 + sup(𝐵, ℝ, < )) = (sup(𝐵, ℝ, < ) + 𝑎))
1514eqeq2d 2747 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑧 = (𝑎 + sup(𝐵, ℝ, < )) ↔ 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)))
1615rexbidva 3169 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < )) ↔ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)))
1716abbidv 2805 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))} = {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)})
1817supeq1d 9295 . . . 4 (𝜑 → sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ))
199, 18eqtrd 2776 . . 3 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ))
20 vex 3445 . . . . . . 7 𝑤 ∈ V
21 eqeq1 2740 . . . . . . . 8 (𝑧 = 𝑤 → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎)))
2221rexbidv 3171 . . . . . . 7 (𝑧 = 𝑤 → (∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ ∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎)))
2320, 22elab 3619 . . . . . 6 (𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ↔ ∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎))
244adantr 481 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → 𝐵 ⊆ ℝ)
255adantr 481 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → 𝐵 ≠ ∅)
266adantr 481 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥)
27 eqid 2736 . . . . . . . . . . 11 {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)} = {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}
2824, 25, 26, 10, 27supaddc 12035 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}, ℝ, < ))
294sselda 3931 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → 𝑏 ∈ ℝ)
3029adantlr 712 . . . . . . . . . . . . . . . 16 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑏 ∈ ℝ)
3130recnd 11096 . . . . . . . . . . . . . . 15 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑏 ∈ ℂ)
3210adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑎 ∈ ℝ)
3332recnd 11096 . . . . . . . . . . . . . . 15 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑎 ∈ ℂ)
3431, 33addcomd 11270 . . . . . . . . . . . . . 14 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑏 + 𝑎) = (𝑎 + 𝑏))
3534eqeq2d 2747 . . . . . . . . . . . . 13 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑧 = (𝑏 + 𝑎) ↔ 𝑧 = (𝑎 + 𝑏)))
3635rexbidva 3169 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑧 = (𝑏 + 𝑎) ↔ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)))
3736abbidv 2805 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)} = {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)})
3837supeq1d 9295 . . . . . . . . . 10 ((𝜑𝑎𝐴) → sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}, ℝ, < ) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ))
3928, 38eqtrd 2776 . . . . . . . . 9 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ))
40 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → (𝑧 = (𝑎 + 𝑏) ↔ 𝑤 = (𝑎 + 𝑏)))
4140rexbidv 3171 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (∃𝑏𝐵 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
4220, 41elab 3619 . . . . . . . . . . . 12 (𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ↔ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏))
43 rspe 3228 . . . . . . . . . . . . . . 15 ((𝑎𝐴 ∧ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
44 oveq1 7336 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑎 → (𝑣 + 𝑏) = (𝑎 + 𝑏))
4544eqeq2d 2747 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑎 → (𝑧 = (𝑣 + 𝑏) ↔ 𝑧 = (𝑎 + 𝑏)))
4645rexbidv 3171 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑎 → (∃𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)))
4746cbvrexvw 3222 . . . . . . . . . . . . . . . . 17 (∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑧 = (𝑎 + 𝑏))
48402rexbidv 3209 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → (∃𝑎𝐴𝑏𝐵 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
4947, 48bitrid 282 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → (∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
50 supadd.c . . . . . . . . . . . . . . . 16 𝐶 = {𝑧 ∣ ∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏)}
5120, 49, 50elab2 3623 . . . . . . . . . . . . . . 15 (𝑤𝐶 ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
5243, 51sylibr 233 . . . . . . . . . . . . . 14 ((𝑎𝐴 ∧ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → 𝑤𝐶)
5352ex 413 . . . . . . . . . . . . 13 (𝑎𝐴 → (∃𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤𝐶))
541sseld 3930 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑎𝐴𝑎 ∈ ℝ))
554sseld 3930 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑏𝐵𝑏 ∈ ℝ))
5654, 55anim12d 609 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)))
57 readdcl 11047 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 + 𝑏) ∈ ℝ)
5856, 57syl6 35 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 + 𝑏) ∈ ℝ))
59 eleq1a 2832 . . . . . . . . . . . . . . . . . 18 ((𝑎 + 𝑏) ∈ ℝ → (𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ))
6058, 59syl6 35 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ)))
6160rexlimdvv 3200 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ))
6251, 61biimtrid 241 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤𝐶𝑤 ∈ ℝ))
6362ssrdv 3937 . . . . . . . . . . . . . 14 (𝜑𝐶 ⊆ ℝ)
64 ovex 7362 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 + 𝑏) ∈ V
6564isseti 3456 . . . . . . . . . . . . . . . . . . . . 21 𝑤 𝑤 = (𝑎 + 𝑏)
6665rgenw 3065 . . . . . . . . . . . . . . . . . . . 20 𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏)
67 r19.2z 4438 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ≠ ∅ ∧ ∀𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏)) → ∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏))
685, 66, 67sylancl 586 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏))
69 rexcom4 3267 . . . . . . . . . . . . . . . . . . 19 (∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏) ↔ ∃𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7068, 69sylib 217 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7170ralrimivw 3143 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
72 r19.2z 4438 . . . . . . . . . . . . . . . . 17 ((𝐴 ≠ ∅ ∧ ∀𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → ∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
732, 71, 72syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
74 rexcom4 3267 . . . . . . . . . . . . . . . 16 (∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏) ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7573, 74sylib 217 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
76 n0 4292 . . . . . . . . . . . . . . . 16 (𝐶 ≠ ∅ ↔ ∃𝑤 𝑤𝐶)
7751exbii 1849 . . . . . . . . . . . . . . . 16 (∃𝑤 𝑤𝐶 ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7876, 77bitri 274 . . . . . . . . . . . . . . 15 (𝐶 ≠ ∅ ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7975, 78sylibr 233 . . . . . . . . . . . . . 14 (𝜑𝐶 ≠ ∅)
801, 2, 3suprcld 12031 . . . . . . . . . . . . . . . 16 (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
8180, 7readdcld 11097 . . . . . . . . . . . . . . 15 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ)
8210adantrr 714 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑎 ∈ ℝ)
8329adantrl 713 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑏 ∈ ℝ)
8480adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → sup(𝐴, ℝ, < ) ∈ ℝ)
857adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → sup(𝐵, ℝ, < ) ∈ ℝ)
861, 2, 33jca 1127 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
87 suprub 12029 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ 𝑎𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
8886, 87sylan 580 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑎𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
8988adantrr 714 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑎 ≤ sup(𝐴, ℝ, < ))
904, 5, 63jca 1127 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥))
91 suprub 12029 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥) ∧ 𝑏𝐵) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9290, 91sylan 580 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9392adantrl 713 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9482, 83, 84, 85, 89, 93le2addd 11687 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
9594ex 413 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
96 breq1 5092 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = (𝑎 + 𝑏) → (𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
9796biimprcd 249 . . . . . . . . . . . . . . . . . . 19 ((𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
9895, 97syl6 35 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))))
9998rexlimdvv 3200 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
10051, 99biimtrid 241 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤𝐶𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
101100ralrimiv 3138 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
102 brralrspcev 5149 . . . . . . . . . . . . . . 15 (((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ ∧ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))) → ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥)
10381, 101, 102syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥)
104 suprub 12029 . . . . . . . . . . . . . . 15 (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) ∧ 𝑤𝐶) → 𝑤 ≤ sup(𝐶, ℝ, < ))
105104ex 413 . . . . . . . . . . . . . 14 ((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) → (𝑤𝐶𝑤 ≤ sup(𝐶, ℝ, < )))
10663, 79, 103, 105syl3anc 1370 . . . . . . . . . . . . 13 (𝜑 → (𝑤𝐶𝑤 ≤ sup(𝐶, ℝ, < )))
10753, 106sylan9r 509 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ sup(𝐶, ℝ, < )))
10842, 107biimtrid 241 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → (𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} → 𝑤 ≤ sup(𝐶, ℝ, < )))
109108ralrimiv 3138 . . . . . . . . . 10 ((𝜑𝑎𝐴) → ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < ))
11032, 30readdcld 11097 . . . . . . . . . . . . . 14 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑎 + 𝑏) ∈ ℝ)
111 eleq1a 2832 . . . . . . . . . . . . . 14 ((𝑎 + 𝑏) ∈ ℝ → (𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
112110, 111syl 17 . . . . . . . . . . . . 13 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
113112rexlimdva 3148 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
114113abssdv 4012 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ⊆ ℝ)
11564isseti 3456 . . . . . . . . . . . . . . . 16 𝑧 𝑧 = (𝑎 + 𝑏)
116115rgenw 3065 . . . . . . . . . . . . . . 15 𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏)
117 r19.2z 4438 . . . . . . . . . . . . . . 15 ((𝐵 ≠ ∅ ∧ ∀𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏)) → ∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏))
1185, 116, 117sylancl 586 . . . . . . . . . . . . . 14 (𝜑 → ∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏))
119 rexcom4 3267 . . . . . . . . . . . . . 14 (∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
120118, 119sylib 217 . . . . . . . . . . . . 13 (𝜑 → ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
121 abn0 4326 . . . . . . . . . . . . 13 ({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅ ↔ ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
122120, 121sylibr 233 . . . . . . . . . . . 12 (𝜑 → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅)
123122adantr 481 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅)
12463, 79, 103suprcld 12031 . . . . . . . . . . . . 13 (𝜑 → sup(𝐶, ℝ, < ) ∈ ℝ)
125124adantr 481 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → sup(𝐶, ℝ, < ) ∈ ℝ)
126 brralrspcev 5149 . . . . . . . . . . . 12 ((sup(𝐶, ℝ, < ) ∈ ℝ ∧ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥)
127125, 109, 126syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥)
128 suprleub 12034 . . . . . . . . . . 11 ((({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥) ∧ sup(𝐶, ℝ, < ) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )))
129114, 123, 127, 125, 128syl31anc 1372 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )))
130109, 129mpbird 256 . . . . . . . . 9 ((𝜑𝑎𝐴) → sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ))
13139, 130eqbrtrd 5111 . . . . . . . 8 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) ≤ sup(𝐶, ℝ, < ))
132 breq1 5092 . . . . . . . 8 (𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → (𝑤 ≤ sup(𝐶, ℝ, < ) ↔ (sup(𝐵, ℝ, < ) + 𝑎) ≤ sup(𝐶, ℝ, < )))
133131, 132syl5ibrcom 246 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑤 ≤ sup(𝐶, ℝ, < )))
134133rexlimdva 3148 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑤 ≤ sup(𝐶, ℝ, < )))
13523, 134biimtrid 241 . . . . 5 (𝜑 → (𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} → 𝑤 ≤ sup(𝐶, ℝ, < )))
136135ralrimiv 3138 . . . 4 (𝜑 → ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < ))
13712, 10readdcld 11097 . . . . . . . 8 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) ∈ ℝ)
138 eleq1a 2832 . . . . . . . 8 ((sup(𝐵, ℝ, < ) + 𝑎) ∈ ℝ → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
139137, 138syl 17 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
140139rexlimdva 3148 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
141140abssdv 4012 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ⊆ ℝ)
142 ovex 7362 . . . . . . . . . 10 (sup(𝐵, ℝ, < ) + 𝑎) ∈ V
143142isseti 3456 . . . . . . . . 9 𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)
144143rgenw 3065 . . . . . . . 8 𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)
145 r19.2z 4438 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)) → ∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
1462, 144, 145sylancl 586 . . . . . . 7 (𝜑 → ∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
147 rexcom4 3267 . . . . . . 7 (∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
148146, 147sylib 217 . . . . . 6 (𝜑 → ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
149 abn0 4326 . . . . . 6 ({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅ ↔ ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
150148, 149sylibr 233 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅)
151 brralrspcev 5149 . . . . . 6 ((sup(𝐶, ℝ, < ) ∈ ℝ ∧ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥)
152124, 136, 151syl2anc 584 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥)
153 suprleub 12034 . . . . 5 ((({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥) ∧ sup(𝐶, ℝ, < ) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )))
154141, 150, 152, 124, 153syl31anc 1372 . . . 4 (𝜑 → (sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )))
155136, 154mpbird 256 . . 3 (𝜑 → sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ))
15619, 155eqbrtrd 5111 . 2 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ≤ sup(𝐶, ℝ, < ))
157 suprleub 12034 . . . 4 (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) ∧ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ) → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
15863, 79, 103, 81, 157syl31anc 1372 . . 3 (𝜑 → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
159101, 158mpbird 256 . 2 (𝜑 → sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
16081, 124letri3d 11210 . 2 (𝜑 → ((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ) ↔ ((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ≤ sup(𝐶, ℝ, < ) ∧ sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))))
161156, 159, 160mpbir2and 710 1 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  {cab 2713  wne 2940  wral 3061  wrex 3070  wss 3897  c0 4268   class class class wbr 5089  (class class class)co 7329  supcsup 9289  cr 10963   + caddc 10967   < clt 11102  cle 11103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-resscn 11021  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-mulcom 11028  ax-addass 11029  ax-mulass 11030  ax-distr 11031  ax-i2m1 11032  ax-1ne0 11033  ax-1rid 11034  ax-rnegex 11035  ax-rrecex 11036  ax-cnre 11037  ax-pre-lttri 11038  ax-pre-lttrn 11039  ax-pre-ltadd 11040  ax-pre-mulgt0 11041  ax-pre-sup 11042
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-opab 5152  df-mpt 5173  df-id 5512  df-po 5526  df-so 5527  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-er 8561  df-en 8797  df-dom 8798  df-sdom 8799  df-sup 9291  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108  df-sub 11300  df-neg 11301
This theorem is referenced by:  ismblfin  35916  itg2addnc  35929  sge0resplit  44270
  Copyright terms: Public domain W3C validator