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

Theorem supadd 11245
Description: The supremum function distributes over addition in a sense similar to that in supmul 11249. (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 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥)
7 suprcl 11237 . . . . . 6 ((𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥) → sup(𝐵, ℝ, < ) ∈ ℝ)
84, 5, 6, 7syl3anc 1490 . . . . 5 (𝜑 → sup(𝐵, ℝ, < ) ∈ ℝ)
9 eqid 2765 . . . . 5 {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))} = {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}
101, 2, 3, 8, 9supaddc 11244 . . . 4 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}, ℝ, < ))
111sselda 3761 . . . . . . . . . 10 ((𝜑𝑎𝐴) → 𝑎 ∈ ℝ)
1211recnd 10322 . . . . . . . . 9 ((𝜑𝑎𝐴) → 𝑎 ∈ ℂ)
138adantr 472 . . . . . . . . . 10 ((𝜑𝑎𝐴) → sup(𝐵, ℝ, < ) ∈ ℝ)
1413recnd 10322 . . . . . . . . 9 ((𝜑𝑎𝐴) → sup(𝐵, ℝ, < ) ∈ ℂ)
1512, 14addcomd 10492 . . . . . . . 8 ((𝜑𝑎𝐴) → (𝑎 + sup(𝐵, ℝ, < )) = (sup(𝐵, ℝ, < ) + 𝑎))
1615eqeq2d 2775 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑧 = (𝑎 + sup(𝐵, ℝ, < )) ↔ 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)))
1716rexbidva 3196 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < )) ↔ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)))
1817abbidv 2884 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))} = {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)})
1918supeq1d 8559 . . . 4 (𝜑 → sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ))
2010, 19eqtrd 2799 . . 3 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ))
21 vex 3353 . . . . . . 7 𝑤 ∈ V
22 eqeq1 2769 . . . . . . . 8 (𝑧 = 𝑤 → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎)))
2322rexbidv 3199 . . . . . . 7 (𝑧 = 𝑤 → (∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ ∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎)))
2421, 23elab 3504 . . . . . 6 (𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ↔ ∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎))
254adantr 472 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → 𝐵 ⊆ ℝ)
265adantr 472 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → 𝐵 ≠ ∅)
276adantr 472 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥)
28 eqid 2765 . . . . . . . . . . 11 {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)} = {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}
2925, 26, 27, 11, 28supaddc 11244 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}, ℝ, < ))
304sselda 3761 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → 𝑏 ∈ ℝ)
3130adantlr 706 . . . . . . . . . . . . . . . 16 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑏 ∈ ℝ)
3231recnd 10322 . . . . . . . . . . . . . . 15 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑏 ∈ ℂ)
3311adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑎 ∈ ℝ)
3433recnd 10322 . . . . . . . . . . . . . . 15 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → 𝑎 ∈ ℂ)
3532, 34addcomd 10492 . . . . . . . . . . . . . 14 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑏 + 𝑎) = (𝑎 + 𝑏))
3635eqeq2d 2775 . . . . . . . . . . . . 13 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑧 = (𝑏 + 𝑎) ↔ 𝑧 = (𝑎 + 𝑏)))
3736rexbidva 3196 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑧 = (𝑏 + 𝑎) ↔ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)))
3837abbidv 2884 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)} = {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)})
3938supeq1d 8559 . . . . . . . . . 10 ((𝜑𝑎𝐴) → sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑏 + 𝑎)}, ℝ, < ) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ))
4029, 39eqtrd 2799 . . . . . . . . 9 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) = sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ))
41 eqeq1 2769 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → (𝑧 = (𝑎 + 𝑏) ↔ 𝑤 = (𝑎 + 𝑏)))
4241rexbidv 3199 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (∃𝑏𝐵 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
4321, 42elab 3504 . . . . . . . . . . . 12 (𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ↔ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏))
44 rspe 3149 . . . . . . . . . . . . . . 15 ((𝑎𝐴 ∧ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
45 oveq1 6849 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑎 → (𝑣 + 𝑏) = (𝑎 + 𝑏))
4645eqeq2d 2775 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑎 → (𝑧 = (𝑣 + 𝑏) ↔ 𝑧 = (𝑎 + 𝑏)))
4746rexbidv 3199 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑎 → (∃𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)))
4847cbvrexv 3320 . . . . . . . . . . . . . . . . 17 (∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑧 = (𝑎 + 𝑏))
49412rexbidv 3204 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → (∃𝑎𝐴𝑏𝐵 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
5048, 49syl5bb 274 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → (∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏)))
51 supadd.c . . . . . . . . . . . . . . . 16 𝐶 = {𝑧 ∣ ∃𝑣𝐴𝑏𝐵 𝑧 = (𝑣 + 𝑏)}
5221, 50, 51elab2 3509 . . . . . . . . . . . . . . 15 (𝑤𝐶 ↔ ∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
5344, 52sylibr 225 . . . . . . . . . . . . . 14 ((𝑎𝐴 ∧ ∃𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → 𝑤𝐶)
5453ex 401 . . . . . . . . . . . . 13 (𝑎𝐴 → (∃𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤𝐶))
551sseld 3760 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑎𝐴𝑎 ∈ ℝ))
564sseld 3760 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑏𝐵𝑏 ∈ ℝ))
5755, 56anim12d 602 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)))
58 readdcl 10272 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 + 𝑏) ∈ ℝ)
5957, 58syl6 35 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 + 𝑏) ∈ ℝ))
60 eleq1a 2839 . . . . . . . . . . . . . . . . . 18 ((𝑎 + 𝑏) ∈ ℝ → (𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ))
6159, 60syl6 35 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ)))
6261rexlimdvv 3184 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ))
6352, 62syl5bi 233 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤𝐶𝑤 ∈ ℝ))
6463ssrdv 3767 . . . . . . . . . . . . . 14 (𝜑𝐶 ⊆ ℝ)
65 ovex 6874 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 + 𝑏) ∈ V
6665isseti 3362 . . . . . . . . . . . . . . . . . . . . 21 𝑤 𝑤 = (𝑎 + 𝑏)
6766rgenw 3071 . . . . . . . . . . . . . . . . . . . 20 𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏)
68 r19.2z 4219 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ≠ ∅ ∧ ∀𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏)) → ∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏))
695, 67, 68sylancl 580 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏))
70 rexcom4 3378 . . . . . . . . . . . . . . . . . . 19 (∃𝑏𝐵𝑤 𝑤 = (𝑎 + 𝑏) ↔ ∃𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7169, 70sylib 209 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7271ralrimivw 3114 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
73 r19.2z 4219 . . . . . . . . . . . . . . . . 17 ((𝐴 ≠ ∅ ∧ ∀𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏)) → ∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
742, 72, 73syl2anc 579 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏))
75 rexcom4 3378 . . . . . . . . . . . . . . . 16 (∃𝑎𝐴𝑤𝑏𝐵 𝑤 = (𝑎 + 𝑏) ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7674, 75sylib 209 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
77 n0 4095 . . . . . . . . . . . . . . . 16 (𝐶 ≠ ∅ ↔ ∃𝑤 𝑤𝐶)
7852exbii 1943 . . . . . . . . . . . . . . . 16 (∃𝑤 𝑤𝐶 ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
7977, 78bitri 266 . . . . . . . . . . . . . . 15 (𝐶 ≠ ∅ ↔ ∃𝑤𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏))
8076, 79sylibr 225 . . . . . . . . . . . . . 14 (𝜑𝐶 ≠ ∅)
81 suprcl 11237 . . . . . . . . . . . . . . . . 17 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) → sup(𝐴, ℝ, < ) ∈ ℝ)
821, 2, 3, 81syl3anc 1490 . . . . . . . . . . . . . . . 16 (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
8382, 8readdcld 10323 . . . . . . . . . . . . . . 15 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ)
8411adantrr 708 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑎 ∈ ℝ)
8530adantrl 707 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑏 ∈ ℝ)
8682adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → sup(𝐴, ℝ, < ) ∈ ℝ)
878adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → sup(𝐵, ℝ, < ) ∈ ℝ)
881, 2, 33jca 1158 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
89 suprub 11238 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ 𝑎𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
9088, 89sylan 575 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑎𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
9190adantrr 708 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑎 ≤ sup(𝐴, ℝ, < ))
924, 5, 63jca 1158 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥))
93 suprub 11238 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐵 𝑦𝑥) ∧ 𝑏𝐵) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9492, 93sylan 575 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9594adantrl 707 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝑏 ≤ sup(𝐵, ℝ, < ))
9684, 85, 86, 87, 91, 95le2addd 10900 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
9796ex 401 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
98 breq1 4812 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = (𝑎 + 𝑏) → (𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
9998biimprcd 241 . . . . . . . . . . . . . . . . . . 19 ((𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
10097, 99syl6 35 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑎𝐴𝑏𝐵) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))))
101100rexlimdvv 3184 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑎𝐴𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
10252, 101syl5bi 233 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤𝐶𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
103102ralrimiv 3112 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
104 brralrspcev 4869 . . . . . . . . . . . . . . 15 (((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ ∧ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))) → ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥)
10583, 103, 104syl2anc 579 . . . . . . . . . . . . . 14 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥)
106 suprub 11238 . . . . . . . . . . . . . . 15 (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) ∧ 𝑤𝐶) → 𝑤 ≤ sup(𝐶, ℝ, < ))
107106ex 401 . . . . . . . . . . . . . 14 ((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) → (𝑤𝐶𝑤 ≤ sup(𝐶, ℝ, < )))
10864, 80, 105, 107syl3anc 1490 . . . . . . . . . . . . 13 (𝜑 → (𝑤𝐶𝑤 ≤ sup(𝐶, ℝ, < )))
10954, 108sylan9r 504 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ sup(𝐶, ℝ, < )))
11043, 109syl5bi 233 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → (𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} → 𝑤 ≤ sup(𝐶, ℝ, < )))
111110ralrimiv 3112 . . . . . . . . . 10 ((𝜑𝑎𝐴) → ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < ))
11233, 31readdcld 10323 . . . . . . . . . . . . . 14 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑎 + 𝑏) ∈ ℝ)
113 eleq1a 2839 . . . . . . . . . . . . . 14 ((𝑎 + 𝑏) ∈ ℝ → (𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
114112, 113syl 17 . . . . . . . . . . . . 13 (((𝜑𝑎𝐴) ∧ 𝑏𝐵) → (𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
115114rexlimdva 3178 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → (∃𝑏𝐵 𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ))
116115abssdv 3836 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ⊆ ℝ)
11765isseti 3362 . . . . . . . . . . . . . . . 16 𝑧 𝑧 = (𝑎 + 𝑏)
118117rgenw 3071 . . . . . . . . . . . . . . 15 𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏)
119 r19.2z 4219 . . . . . . . . . . . . . . 15 ((𝐵 ≠ ∅ ∧ ∀𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏)) → ∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏))
1205, 118, 119sylancl 580 . . . . . . . . . . . . . 14 (𝜑 → ∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏))
121 rexcom4 3378 . . . . . . . . . . . . . 14 (∃𝑏𝐵𝑧 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
122120, 121sylib 209 . . . . . . . . . . . . 13 (𝜑 → ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
123 abn0 4119 . . . . . . . . . . . . 13 ({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅ ↔ ∃𝑧𝑏𝐵 𝑧 = (𝑎 + 𝑏))
124122, 123sylibr 225 . . . . . . . . . . . 12 (𝜑 → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅)
125124adantr 472 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅)
126 suprcl 11237 . . . . . . . . . . . . . 14 ((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) → sup(𝐶, ℝ, < ) ∈ ℝ)
12764, 80, 105, 126syl3anc 1490 . . . . . . . . . . . . 13 (𝜑 → sup(𝐶, ℝ, < ) ∈ ℝ)
128127adantr 472 . . . . . . . . . . . 12 ((𝜑𝑎𝐴) → sup(𝐶, ℝ, < ) ∈ ℝ)
129 brralrspcev 4869 . . . . . . . . . . . 12 ((sup(𝐶, ℝ, < ) ∈ ℝ ∧ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥)
130128, 111, 129syl2anc 579 . . . . . . . . . . 11 ((𝜑𝑎𝐴) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥)
131 suprleub 11243 . . . . . . . . . . 11 ((({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤𝑥) ∧ sup(𝐶, ℝ, < ) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )))
132116, 125, 130, 128, 131syl31anc 1492 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )))
133111, 132mpbird 248 . . . . . . . . 9 ((𝜑𝑎𝐴) → sup({𝑧 ∣ ∃𝑏𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ))
13440, 133eqbrtrd 4831 . . . . . . . 8 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) ≤ sup(𝐶, ℝ, < ))
135 breq1 4812 . . . . . . . 8 (𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → (𝑤 ≤ sup(𝐶, ℝ, < ) ↔ (sup(𝐵, ℝ, < ) + 𝑎) ≤ sup(𝐶, ℝ, < )))
136134, 135syl5ibrcom 238 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑤 ≤ sup(𝐶, ℝ, < )))
137136rexlimdva 3178 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑤 ≤ sup(𝐶, ℝ, < )))
13824, 137syl5bi 233 . . . . 5 (𝜑 → (𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} → 𝑤 ≤ sup(𝐶, ℝ, < )))
139138ralrimiv 3112 . . . 4 (𝜑 → ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < ))
14013, 11readdcld 10323 . . . . . . . 8 ((𝜑𝑎𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) ∈ ℝ)
141 eleq1a 2839 . . . . . . . 8 ((sup(𝐵, ℝ, < ) + 𝑎) ∈ ℝ → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
142140, 141syl 17 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
143142rexlimdva 3178 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ))
144143abssdv 3836 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ⊆ ℝ)
145 ovex 6874 . . . . . . . . . 10 (sup(𝐵, ℝ, < ) + 𝑎) ∈ V
146145isseti 3362 . . . . . . . . 9 𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)
147146rgenw 3071 . . . . . . . 8 𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)
148 r19.2z 4219 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)) → ∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
1492, 147, 148sylancl 580 . . . . . . 7 (𝜑 → ∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
150 rexcom4 3378 . . . . . . 7 (∃𝑎𝐴𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
151149, 150sylib 209 . . . . . 6 (𝜑 → ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
152 abn0 4119 . . . . . 6 ({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅ ↔ ∃𝑧𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))
153151, 152sylibr 225 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅)
154 brralrspcev 4869 . . . . . 6 ((sup(𝐶, ℝ, < ) ∈ ℝ ∧ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥)
155127, 139, 154syl2anc 579 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥)
156 suprleub 11243 . . . . 5 ((({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤𝑥) ∧ sup(𝐶, ℝ, < ) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )))
157144, 153, 155, 127, 156syl31anc 1492 . . . 4 (𝜑 → (sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )))
158139, 157mpbird 248 . . 3 (𝜑 → sup({𝑧 ∣ ∃𝑎𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ))
15920, 158eqbrtrd 4831 . 2 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ≤ sup(𝐶, ℝ, < ))
160 suprleub 11243 . . . 4 (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) ∧ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ) → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
16164, 80, 105, 83, 160syl31anc 1492 . . 3 (𝜑 → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))
162103, 161mpbird 248 . 2 (𝜑 → sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))
16383, 127letri3d 10433 . 2 (𝜑 → ((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ) ↔ ((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ≤ sup(𝐶, ℝ, < ) ∧ sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))))
164159, 162, 163mpbir2and 704 1 (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  {cab 2751  wne 2937  wral 3055  wrex 3056  wss 3732  c0 4079   class class class wbr 4809  (class class class)co 6842  supcsup 8553  cr 10188   + caddc 10192   < clt 10328  cle 10329
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-po 5198  df-so 5199  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-sup 8555  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523
This theorem is referenced by:  ismblfin  33806  itg2addnc  33819  sge0resplit  41192
  Copyright terms: Public domain W3C validator