Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  xrofsup Structured version   Visualization version   GIF version

Theorem xrofsup 32449
Description: The supremum is preserved by extended addition set operation. (Provided minus infinity is not involved as it does not behave well with addition.) (Contributed by Thierry Arnoux, 20-Mar-2017.)
Hypotheses
Ref Expression
xrofsup.1 (𝜑𝑋 ⊆ ℝ*)
xrofsup.2 (𝜑𝑌 ⊆ ℝ*)
xrofsup.3 (𝜑 → sup(𝑋, ℝ*, < ) ≠ -∞)
xrofsup.4 (𝜑 → sup(𝑌, ℝ*, < ) ≠ -∞)
xrofsup.5 (𝜑𝑍 = ( +𝑒 “ (𝑋 × 𝑌)))
Assertion
Ref Expression
xrofsup (𝜑 → sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))

Proof of Theorem xrofsup
Dummy variables 𝑎 𝑏 𝑘 𝑢 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrofsup.5 . . 3 (𝜑𝑍 = ( +𝑒 “ (𝑋 × 𝑌)))
2 xrofsup.1 . . . . . . . . . 10 (𝜑𝑋 ⊆ ℝ*)
32sseld 3973 . . . . . . . . 9 (𝜑 → (𝑥𝑋𝑥 ∈ ℝ*))
4 xrofsup.2 . . . . . . . . . 10 (𝜑𝑌 ⊆ ℝ*)
54sseld 3973 . . . . . . . . 9 (𝜑 → (𝑦𝑌𝑦 ∈ ℝ*))
63, 5anim12d 608 . . . . . . . 8 (𝜑 → ((𝑥𝑋𝑦𝑌) → (𝑥 ∈ ℝ*𝑦 ∈ ℝ*)))
76imp 406 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 ∈ ℝ*𝑦 ∈ ℝ*))
8 xaddcl 13215 . . . . . . 7 ((𝑥 ∈ ℝ*𝑦 ∈ ℝ*) → (𝑥 +𝑒 𝑦) ∈ ℝ*)
97, 8syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 +𝑒 𝑦) ∈ ℝ*)
109ralrimivva 3192 . . . . 5 (𝜑 → ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ∈ ℝ*)
11 fveq2 6881 . . . . . . . 8 (𝑢 = ⟨𝑥, 𝑦⟩ → ( +𝑒𝑢) = ( +𝑒 ‘⟨𝑥, 𝑦⟩))
12 df-ov 7404 . . . . . . . 8 (𝑥 +𝑒 𝑦) = ( +𝑒 ‘⟨𝑥, 𝑦⟩)
1311, 12eqtr4di 2782 . . . . . . 7 (𝑢 = ⟨𝑥, 𝑦⟩ → ( +𝑒𝑢) = (𝑥 +𝑒 𝑦))
1413eleq1d 2810 . . . . . 6 (𝑢 = ⟨𝑥, 𝑦⟩ → (( +𝑒𝑢) ∈ ℝ* ↔ (𝑥 +𝑒 𝑦) ∈ ℝ*))
1514ralxp 5831 . . . . 5 (∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ* ↔ ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ∈ ℝ*)
1610, 15sylibr 233 . . . 4 (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*)
17 xaddf 13200 . . . . . 6 +𝑒 :(ℝ* × ℝ*)⟶ℝ*
18 ffun 6710 . . . . . 6 ( +𝑒 :(ℝ* × ℝ*)⟶ℝ* → Fun +𝑒 )
1917, 18ax-mp 5 . . . . 5 Fun +𝑒
20 xpss12 5681 . . . . . . 7 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → (𝑋 × 𝑌) ⊆ (ℝ* × ℝ*))
212, 4, 20syl2anc 583 . . . . . 6 (𝜑 → (𝑋 × 𝑌) ⊆ (ℝ* × ℝ*))
2217fdmi 6719 . . . . . 6 dom +𝑒 = (ℝ* × ℝ*)
2321, 22sseqtrrdi 4025 . . . . 5 (𝜑 → (𝑋 × 𝑌) ⊆ dom +𝑒 )
24 funimass4 6946 . . . . 5 ((Fun +𝑒 ∧ (𝑋 × 𝑌) ⊆ dom +𝑒 ) → (( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*))
2519, 23, 24sylancr 586 . . . 4 (𝜑 → (( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*))
2616, 25mpbird 257 . . 3 (𝜑 → ( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ*)
271, 26eqsstrd 4012 . 2 (𝜑𝑍 ⊆ ℝ*)
28 supxrcl 13291 . . . 4 (𝑋 ⊆ ℝ* → sup(𝑋, ℝ*, < ) ∈ ℝ*)
292, 28syl 17 . . 3 (𝜑 → sup(𝑋, ℝ*, < ) ∈ ℝ*)
30 supxrcl 13291 . . . 4 (𝑌 ⊆ ℝ* → sup(𝑌, ℝ*, < ) ∈ ℝ*)
314, 30syl 17 . . 3 (𝜑 → sup(𝑌, ℝ*, < ) ∈ ℝ*)
3229, 31xaddcld 13277 . 2 (𝜑 → (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∈ ℝ*)
331eleq2d 2811 . . . . 5 (𝜑 → (𝑧𝑍𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))))
3433pm5.32i 574 . . . 4 ((𝜑𝑧𝑍) ↔ (𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))))
35 nfvd 1910 . . . . 5 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑥 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
36 nfvd 1910 . . . . 5 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑦 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
372ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑋 ⊆ ℝ*)
38 simprl 768 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
39 supxrub 13300 . . . . . . . . . . 11 ((𝑋 ⊆ ℝ*𝑥𝑋) → 𝑥 ≤ sup(𝑋, ℝ*, < ))
4037, 38, 39syl2anc 583 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥 ≤ sup(𝑋, ℝ*, < ))
414ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑌 ⊆ ℝ*)
42 simprr 770 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
43 supxrub 13300 . . . . . . . . . . 11 ((𝑌 ⊆ ℝ*𝑦𝑌) → 𝑦 ≤ sup(𝑌, ℝ*, < ))
4441, 42, 43syl2anc 583 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦 ≤ sup(𝑌, ℝ*, < ))
4537, 38sseldd 3975 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥 ∈ ℝ*)
4641, 42sseldd 3975 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦 ∈ ℝ*)
4737, 28syl 17 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → sup(𝑋, ℝ*, < ) ∈ ℝ*)
4841, 30syl 17 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → sup(𝑌, ℝ*, < ) ∈ ℝ*)
49 xle2add 13235 . . . . . . . . . . 11 (((𝑥 ∈ ℝ*𝑦 ∈ ℝ*) ∧ (sup(𝑋, ℝ*, < ) ∈ ℝ* ∧ sup(𝑌, ℝ*, < ) ∈ ℝ*)) → ((𝑥 ≤ sup(𝑋, ℝ*, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ*, < )) → (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
5045, 46, 47, 48, 49syl22anc 836 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥 ≤ sup(𝑋, ℝ*, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ*, < )) → (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
5140, 44, 50mp2and 696 . . . . . . . . 9 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
5251ralrimivva 3192 . . . . . . . 8 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
53 fvelima 6947 . . . . . . . . . . 11 ((Fun +𝑒𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5419, 53mpan 687 . . . . . . . . . 10 (𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌)) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5554adantl 481 . . . . . . . . 9 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5613eqeq1d 2726 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (( +𝑒𝑢) = 𝑧 ↔ (𝑥 +𝑒 𝑦) = 𝑧))
5756rexxp 5832 . . . . . . . . 9 (∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧 ↔ ∃𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) = 𝑧)
5855, 57sylib 217 . . . . . . . 8 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) = 𝑧)
5952, 58r19.29d2r 3132 . . . . . . 7 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ (𝑥 +𝑒 𝑦) = 𝑧))
60 ancom 460 . . . . . . . 8 (((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ (𝑥 +𝑒 𝑦) = 𝑧) ↔ ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
61602rexbii 3121 . . . . . . 7 (∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ (𝑥 +𝑒 𝑦) = 𝑧) ↔ ∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
6259, 61sylib 217 . . . . . 6 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
63 breq1 5141 . . . . . . . . 9 ((𝑥 +𝑒 𝑦) = 𝑧 → ((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ↔ 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
6463biimpa 476 . . . . . . . 8 (((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6564reximi 3076 . . . . . . 7 (∃𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6665reximi 3076 . . . . . 6 (∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑥𝑋𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6762, 66syl 17 . . . . 5 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6835, 36, 6719.9d2r 32181 . . . 4 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6934, 68sylbi 216 . . 3 ((𝜑𝑧𝑍) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
7069ralrimiva 3138 . 2 (𝜑 → ∀𝑧𝑍 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
712ad2antrr 723 . . . . . 6 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑋 ⊆ ℝ*)
724ad2antrr 723 . . . . . 6 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑌 ⊆ ℝ*)
73 simplr 766 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑧 ∈ ℝ)
7429ad2antrr 723 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑋, ℝ*, < ) ∈ ℝ*)
7531ad2antrr 723 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑌, ℝ*, < ) ∈ ℝ*)
76 xrofsup.3 . . . . . . . 8 (𝜑 → sup(𝑋, ℝ*, < ) ≠ -∞)
7776ad2antrr 723 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑋, ℝ*, < ) ≠ -∞)
78 xrofsup.4 . . . . . . . 8 (𝜑 → sup(𝑌, ℝ*, < ) ≠ -∞)
7978ad2antrr 723 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑌, ℝ*, < ) ≠ -∞)
80 simpr 484 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
8173, 74, 75, 77, 79, 80xlt2addrd 32440 . . . . . 6 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
82 nfv 1909 . . . . . . . 8 𝑏(𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*)
83 nfcv 2895 . . . . . . . . 9 𝑏*
84 nfre1 3274 . . . . . . . . 9 𝑏𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))
8583, 84nfrexw 3302 . . . . . . . 8 𝑏𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))
8682, 85nfan 1894 . . . . . . 7 𝑏((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
87 nfvd 1910 . . . . . . 7 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → Ⅎ𝑎𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
88 nfvd 1910 . . . . . . 7 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → Ⅎ𝑏𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
89 id 22 . . . . . . . . . . . 12 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9089ralrimivw 3142 . . . . . . . . . . 11 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → ∀𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9190ralrimivw 3142 . . . . . . . . . 10 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → ∀𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9291adantr 480 . . . . . . . . 9 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∀𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
93 simpr 484 . . . . . . . . 9 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
9492, 93r19.29d2r 3132 . . . . . . . 8 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))))
95 simplrr 775 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ (𝑣𝑋𝑤𝑌 ∧ (𝑎 < 𝑣𝑏 < 𝑤))) → (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
96953anassrs 1357 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
9796simp1d 1139 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑧 = (𝑎 +𝑒 𝑏))
98 simp-4l 780 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 ∈ ℝ*𝑏 ∈ ℝ*))
99 simplrl 774 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ (𝑣𝑋𝑤𝑌 ∧ (𝑎 < 𝑣𝑏 < 𝑤))) → (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
100993anassrs 1357 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
101100simpld 494 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑋 ⊆ ℝ*)
102 simpllr 773 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑣𝑋)
103101, 102sseldd 3975 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑣 ∈ ℝ*)
104100simprd 495 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑌 ⊆ ℝ*)
105 simplr 766 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑤𝑌)
106104, 105sseldd 3975 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑤 ∈ ℝ*)
10798, 103, 106jca32 515 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)))
108 simpr 484 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 < 𝑣𝑏 < 𝑤))
109 xlt2add 13236 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) → ((𝑎 < 𝑣𝑏 < 𝑤) → (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤)))
110109imp 406 . . . . . . . . . . . . . 14 ((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤))
111 breq1 5141 . . . . . . . . . . . . . . 15 (𝑧 = (𝑎 +𝑒 𝑏) → (𝑧 < (𝑣 +𝑒 𝑤) ↔ (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤)))
112111biimpar 477 . . . . . . . . . . . . . 14 ((𝑧 = (𝑎 +𝑒 𝑏) ∧ (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤)) → 𝑧 < (𝑣 +𝑒 𝑤))
113110, 112sylan2 592 . . . . . . . . . . . . 13 ((𝑧 = (𝑎 +𝑒 𝑏) ∧ (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) ∧ (𝑎 < 𝑣𝑏 < 𝑤))) → 𝑧 < (𝑣 +𝑒 𝑤))
11497, 107, 108, 113syl12anc 834 . . . . . . . . . . . 12 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑧 < (𝑣 +𝑒 𝑤))
115 simplll 772 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑋 ⊆ ℝ*)
116 simprl 768 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑎 ∈ ℝ*)
117 simplr2 1213 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑎 < sup(𝑋, ℝ*, < ))
118 supxrlub 13301 . . . . . . . . . . . . . . . 16 ((𝑋 ⊆ ℝ*𝑎 ∈ ℝ*) → (𝑎 < sup(𝑋, ℝ*, < ) ↔ ∃𝑣𝑋 𝑎 < 𝑣))
119118biimpa 476 . . . . . . . . . . . . . . 15 (((𝑋 ⊆ ℝ*𝑎 ∈ ℝ*) ∧ 𝑎 < sup(𝑋, ℝ*, < )) → ∃𝑣𝑋 𝑎 < 𝑣)
120115, 116, 117, 119syl21anc 835 . . . . . . . . . . . . . 14 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑣𝑋 𝑎 < 𝑣)
121 simpllr 773 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑌 ⊆ ℝ*)
122 simprr 770 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑏 ∈ ℝ*)
123 simplr3 1214 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑏 < sup(𝑌, ℝ*, < ))
124 supxrlub 13301 . . . . . . . . . . . . . . . 16 ((𝑌 ⊆ ℝ*𝑏 ∈ ℝ*) → (𝑏 < sup(𝑌, ℝ*, < ) ↔ ∃𝑤𝑌 𝑏 < 𝑤))
125124biimpa 476 . . . . . . . . . . . . . . 15 (((𝑌 ⊆ ℝ*𝑏 ∈ ℝ*) ∧ 𝑏 < sup(𝑌, ℝ*, < )) → ∃𝑤𝑌 𝑏 < 𝑤)
126121, 122, 123, 125syl21anc 835 . . . . . . . . . . . . . 14 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑤𝑌 𝑏 < 𝑤)
127 reeanv 3218 . . . . . . . . . . . . . 14 (∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤) ↔ (∃𝑣𝑋 𝑎 < 𝑣 ∧ ∃𝑤𝑌 𝑏 < 𝑤))
128120, 126, 127sylanbrc 582 . . . . . . . . . . . . 13 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤))
129128ancoms 458 . . . . . . . . . . . 12 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) → ∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤))
130114, 129reximddv2 3204 . . . . . . . . . . 11 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
131130ex 412 . . . . . . . . . 10 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤)))
132131reximdva 3160 . . . . . . . . 9 (𝑎 ∈ ℝ* → (∃𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤)))
133132reximia 3073 . . . . . . . 8 (∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13494, 133syl 17 . . . . . . 7 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13586, 87, 88, 13419.9d2rf 32180 . . . . . 6 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13671, 72, 81, 135syl21anc 835 . . . . 5 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
137 simprl 768 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → 𝑣𝑋)
138 simprr 770 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → 𝑤𝑌)
13919a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → Fun +𝑒 )
14023adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑋 × 𝑌) ⊆ dom +𝑒 )
141137, 138, 139, 140elovimad 7449 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌)))
1421eleq2d 2811 . . . . . . . . . 10 (𝜑 → ((𝑣 +𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌))))
143142adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → ((𝑣 +𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌))))
144141, 143mpbird 257 . . . . . . . 8 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑣 +𝑒 𝑤) ∈ 𝑍)
145 simpr 484 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝑋𝑤𝑌)) ∧ 𝑘 = (𝑣 +𝑒 𝑤)) → 𝑘 = (𝑣 +𝑒 𝑤))
146145breq2d 5150 . . . . . . . 8 (((𝜑 ∧ (𝑣𝑋𝑤𝑌)) ∧ 𝑘 = (𝑣 +𝑒 𝑤)) → (𝑧 < 𝑘𝑧 < (𝑣 +𝑒 𝑤)))
147144, 146rspcedv 3597 . . . . . . 7 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
148147rexlimdvva 3203 . . . . . 6 (𝜑 → (∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
149148ad2antrr 723 . . . . 5 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → (∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
150136, 149mpd 15 . . . 4 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑘𝑍 𝑧 < 𝑘)
151150ex 412 . . 3 ((𝜑𝑧 ∈ ℝ) → (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))
152151ralrimiva 3138 . 2 (𝜑 → ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))
153 supxr2 13290 . 2 (((𝑍 ⊆ ℝ* ∧ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∈ ℝ*) ∧ (∀𝑧𝑍 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))) → sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
15427, 32, 70, 152, 153syl22anc 836 1 (𝜑 → sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  wne 2932  wral 3053  wrex 3062  wss 3940  cop 4626   class class class wbr 5138   × cxp 5664  dom cdm 5666  cima 5669  Fun wfun 6527  wf 6529  cfv 6533  (class class class)co 7401  supcsup 9431  cr 11105  -∞cmnf 11243  *cxr 11244   < clt 11245  cle 11246   +𝑒 cxad 13087
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-po 5578  df-so 5579  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-sup 9433  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-2 12272  df-rp 12972  df-xneg 13089  df-xadd 13090
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator