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 31672
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 3943 . . . . . . . . 9 (𝜑 → (𝑥𝑋𝑥 ∈ ℝ*))
4 xrofsup.2 . . . . . . . . . 10 (𝜑𝑌 ⊆ ℝ*)
54sseld 3943 . . . . . . . . 9 (𝜑 → (𝑦𝑌𝑦 ∈ ℝ*))
63, 5anim12d 609 . . . . . . . 8 (𝜑 → ((𝑥𝑋𝑦𝑌) → (𝑥 ∈ ℝ*𝑦 ∈ ℝ*)))
76imp 407 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 ∈ ℝ*𝑦 ∈ ℝ*))
8 xaddcl 13158 . . . . . . 7 ((𝑥 ∈ ℝ*𝑦 ∈ ℝ*) → (𝑥 +𝑒 𝑦) ∈ ℝ*)
97, 8syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 +𝑒 𝑦) ∈ ℝ*)
109ralrimivva 3197 . . . . 5 (𝜑 → ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ∈ ℝ*)
11 fveq2 6842 . . . . . . . 8 (𝑢 = ⟨𝑥, 𝑦⟩ → ( +𝑒𝑢) = ( +𝑒 ‘⟨𝑥, 𝑦⟩))
12 df-ov 7360 . . . . . . . 8 (𝑥 +𝑒 𝑦) = ( +𝑒 ‘⟨𝑥, 𝑦⟩)
1311, 12eqtr4di 2794 . . . . . . 7 (𝑢 = ⟨𝑥, 𝑦⟩ → ( +𝑒𝑢) = (𝑥 +𝑒 𝑦))
1413eleq1d 2822 . . . . . 6 (𝑢 = ⟨𝑥, 𝑦⟩ → (( +𝑒𝑢) ∈ ℝ* ↔ (𝑥 +𝑒 𝑦) ∈ ℝ*))
1514ralxp 5797 . . . . 5 (∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ* ↔ ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ∈ ℝ*)
1610, 15sylibr 233 . . . 4 (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*)
17 xaddf 13143 . . . . . 6 +𝑒 :(ℝ* × ℝ*)⟶ℝ*
18 ffun 6671 . . . . . 6 ( +𝑒 :(ℝ* × ℝ*)⟶ℝ* → Fun +𝑒 )
1917, 18ax-mp 5 . . . . 5 Fun +𝑒
20 xpss12 5648 . . . . . . 7 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → (𝑋 × 𝑌) ⊆ (ℝ* × ℝ*))
212, 4, 20syl2anc 584 . . . . . 6 (𝜑 → (𝑋 × 𝑌) ⊆ (ℝ* × ℝ*))
2217fdmi 6680 . . . . . 6 dom +𝑒 = (ℝ* × ℝ*)
2321, 22sseqtrrdi 3995 . . . . 5 (𝜑 → (𝑋 × 𝑌) ⊆ dom +𝑒 )
24 funimass4 6907 . . . . 5 ((Fun +𝑒 ∧ (𝑋 × 𝑌) ⊆ dom +𝑒 ) → (( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*))
2519, 23, 24sylancr 587 . . . 4 (𝜑 → (( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*))
2616, 25mpbird 256 . . 3 (𝜑 → ( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ*)
271, 26eqsstrd 3982 . 2 (𝜑𝑍 ⊆ ℝ*)
28 supxrcl 13234 . . . 4 (𝑋 ⊆ ℝ* → sup(𝑋, ℝ*, < ) ∈ ℝ*)
292, 28syl 17 . . 3 (𝜑 → sup(𝑋, ℝ*, < ) ∈ ℝ*)
30 supxrcl 13234 . . . 4 (𝑌 ⊆ ℝ* → sup(𝑌, ℝ*, < ) ∈ ℝ*)
314, 30syl 17 . . 3 (𝜑 → sup(𝑌, ℝ*, < ) ∈ ℝ*)
3229, 31xaddcld 13220 . 2 (𝜑 → (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∈ ℝ*)
331eleq2d 2823 . . . . 5 (𝜑 → (𝑧𝑍𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))))
3433pm5.32i 575 . . . 4 ((𝜑𝑧𝑍) ↔ (𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))))
35 nfvd 1918 . . . . 5 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑥 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
36 nfvd 1918 . . . . 5 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑦 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
372ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑋 ⊆ ℝ*)
38 simprl 769 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
39 supxrub 13243 . . . . . . . . . . 11 ((𝑋 ⊆ ℝ*𝑥𝑋) → 𝑥 ≤ sup(𝑋, ℝ*, < ))
4037, 38, 39syl2anc 584 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥 ≤ sup(𝑋, ℝ*, < ))
414ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑌 ⊆ ℝ*)
42 simprr 771 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
43 supxrub 13243 . . . . . . . . . . 11 ((𝑌 ⊆ ℝ*𝑦𝑌) → 𝑦 ≤ sup(𝑌, ℝ*, < ))
4441, 42, 43syl2anc 584 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦 ≤ sup(𝑌, ℝ*, < ))
4537, 38sseldd 3945 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥 ∈ ℝ*)
4641, 42sseldd 3945 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦 ∈ ℝ*)
4737, 28syl 17 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → sup(𝑋, ℝ*, < ) ∈ ℝ*)
4841, 30syl 17 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → sup(𝑌, ℝ*, < ) ∈ ℝ*)
49 xle2add 13178 . . . . . . . . . . 11 (((𝑥 ∈ ℝ*𝑦 ∈ ℝ*) ∧ (sup(𝑋, ℝ*, < ) ∈ ℝ* ∧ sup(𝑌, ℝ*, < ) ∈ ℝ*)) → ((𝑥 ≤ sup(𝑋, ℝ*, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ*, < )) → (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
5045, 46, 47, 48, 49syl22anc 837 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥 ≤ sup(𝑋, ℝ*, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ*, < )) → (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
5140, 44, 50mp2and 697 . . . . . . . . 9 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
5251ralrimivva 3197 . . . . . . . 8 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
53 fvelima 6908 . . . . . . . . . . 11 ((Fun +𝑒𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5419, 53mpan 688 . . . . . . . . . 10 (𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌)) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5554adantl 482 . . . . . . . . 9 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5613eqeq1d 2738 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (( +𝑒𝑢) = 𝑧 ↔ (𝑥 +𝑒 𝑦) = 𝑧))
5756rexxp 5798 . . . . . . . . 9 (∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧 ↔ ∃𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) = 𝑧)
5855, 57sylib 217 . . . . . . . 8 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) = 𝑧)
5952, 58r19.29d2r 3137 . . . . . . 7 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ (𝑥 +𝑒 𝑦) = 𝑧))
60 ancom 461 . . . . . . . 8 (((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ (𝑥 +𝑒 𝑦) = 𝑧) ↔ ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
61602rexbii 3128 . . . . . . 7 (∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ (𝑥 +𝑒 𝑦) = 𝑧) ↔ ∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
6259, 61sylib 217 . . . . . 6 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
63 breq1 5108 . . . . . . . . 9 ((𝑥 +𝑒 𝑦) = 𝑧 → ((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ↔ 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
6463biimpa 477 . . . . . . . 8 (((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6564reximi 3087 . . . . . . 7 (∃𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6665reximi 3087 . . . . . 6 (∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑥𝑋𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6762, 66syl 17 . . . . 5 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6835, 36, 6719.9d2r 31401 . . . 4 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6934, 68sylbi 216 . . 3 ((𝜑𝑧𝑍) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
7069ralrimiva 3143 . 2 (𝜑 → ∀𝑧𝑍 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
712ad2antrr 724 . . . . . 6 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑋 ⊆ ℝ*)
724ad2antrr 724 . . . . . 6 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑌 ⊆ ℝ*)
73 simplr 767 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑧 ∈ ℝ)
7429ad2antrr 724 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑋, ℝ*, < ) ∈ ℝ*)
7531ad2antrr 724 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑌, ℝ*, < ) ∈ ℝ*)
76 xrofsup.3 . . . . . . . 8 (𝜑 → sup(𝑋, ℝ*, < ) ≠ -∞)
7776ad2antrr 724 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑋, ℝ*, < ) ≠ -∞)
78 xrofsup.4 . . . . . . . 8 (𝜑 → sup(𝑌, ℝ*, < ) ≠ -∞)
7978ad2antrr 724 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑌, ℝ*, < ) ≠ -∞)
80 simpr 485 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
8173, 74, 75, 77, 79, 80xlt2addrd 31663 . . . . . 6 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
82 nfv 1917 . . . . . . . 8 𝑏(𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*)
83 nfcv 2907 . . . . . . . . 9 𝑏*
84 nfre1 3268 . . . . . . . . 9 𝑏𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))
8583, 84nfrexw 3296 . . . . . . . 8 𝑏𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))
8682, 85nfan 1902 . . . . . . 7 𝑏((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
87 nfvd 1918 . . . . . . 7 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → Ⅎ𝑎𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
88 nfvd 1918 . . . . . . 7 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → Ⅎ𝑏𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
89 id 22 . . . . . . . . . . . 12 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9089ralrimivw 3147 . . . . . . . . . . 11 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → ∀𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9190ralrimivw 3147 . . . . . . . . . 10 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → ∀𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9291adantr 481 . . . . . . . . 9 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∀𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
93 simpr 485 . . . . . . . . 9 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
9492, 93r19.29d2r 3137 . . . . . . . 8 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))))
95 simplrr 776 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ (𝑣𝑋𝑤𝑌 ∧ (𝑎 < 𝑣𝑏 < 𝑤))) → (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
96953anassrs 1360 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
9796simp1d 1142 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑧 = (𝑎 +𝑒 𝑏))
98 simp-4l 781 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 ∈ ℝ*𝑏 ∈ ℝ*))
99 simplrl 775 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ (𝑣𝑋𝑤𝑌 ∧ (𝑎 < 𝑣𝑏 < 𝑤))) → (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
100993anassrs 1360 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
101100simpld 495 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑋 ⊆ ℝ*)
102 simpllr 774 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑣𝑋)
103101, 102sseldd 3945 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑣 ∈ ℝ*)
104100simprd 496 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑌 ⊆ ℝ*)
105 simplr 767 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑤𝑌)
106104, 105sseldd 3945 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑤 ∈ ℝ*)
10798, 103, 106jca32 516 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)))
108 simpr 485 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 < 𝑣𝑏 < 𝑤))
109 xlt2add 13179 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) → ((𝑎 < 𝑣𝑏 < 𝑤) → (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤)))
110109imp 407 . . . . . . . . . . . . . 14 ((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤))
111 breq1 5108 . . . . . . . . . . . . . . 15 (𝑧 = (𝑎 +𝑒 𝑏) → (𝑧 < (𝑣 +𝑒 𝑤) ↔ (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤)))
112111biimpar 478 . . . . . . . . . . . . . 14 ((𝑧 = (𝑎 +𝑒 𝑏) ∧ (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤)) → 𝑧 < (𝑣 +𝑒 𝑤))
113110, 112sylan2 593 . . . . . . . . . . . . 13 ((𝑧 = (𝑎 +𝑒 𝑏) ∧ (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) ∧ (𝑎 < 𝑣𝑏 < 𝑤))) → 𝑧 < (𝑣 +𝑒 𝑤))
11497, 107, 108, 113syl12anc 835 . . . . . . . . . . . 12 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑧 < (𝑣 +𝑒 𝑤))
115 simplll 773 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑋 ⊆ ℝ*)
116 simprl 769 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑎 ∈ ℝ*)
117 simplr2 1216 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑎 < sup(𝑋, ℝ*, < ))
118 supxrlub 13244 . . . . . . . . . . . . . . . 16 ((𝑋 ⊆ ℝ*𝑎 ∈ ℝ*) → (𝑎 < sup(𝑋, ℝ*, < ) ↔ ∃𝑣𝑋 𝑎 < 𝑣))
119118biimpa 477 . . . . . . . . . . . . . . 15 (((𝑋 ⊆ ℝ*𝑎 ∈ ℝ*) ∧ 𝑎 < sup(𝑋, ℝ*, < )) → ∃𝑣𝑋 𝑎 < 𝑣)
120115, 116, 117, 119syl21anc 836 . . . . . . . . . . . . . 14 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑣𝑋 𝑎 < 𝑣)
121 simpllr 774 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑌 ⊆ ℝ*)
122 simprr 771 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑏 ∈ ℝ*)
123 simplr3 1217 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑏 < sup(𝑌, ℝ*, < ))
124 supxrlub 13244 . . . . . . . . . . . . . . . 16 ((𝑌 ⊆ ℝ*𝑏 ∈ ℝ*) → (𝑏 < sup(𝑌, ℝ*, < ) ↔ ∃𝑤𝑌 𝑏 < 𝑤))
125124biimpa 477 . . . . . . . . . . . . . . 15 (((𝑌 ⊆ ℝ*𝑏 ∈ ℝ*) ∧ 𝑏 < sup(𝑌, ℝ*, < )) → ∃𝑤𝑌 𝑏 < 𝑤)
126121, 122, 123, 125syl21anc 836 . . . . . . . . . . . . . 14 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑤𝑌 𝑏 < 𝑤)
127 reeanv 3217 . . . . . . . . . . . . . 14 (∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤) ↔ (∃𝑣𝑋 𝑎 < 𝑣 ∧ ∃𝑤𝑌 𝑏 < 𝑤))
128120, 126, 127sylanbrc 583 . . . . . . . . . . . . 13 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤))
129128ancoms 459 . . . . . . . . . . . 12 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) → ∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤))
130114, 129reximddv2 3206 . . . . . . . . . . 11 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
131130ex 413 . . . . . . . . . 10 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤)))
132131reximdva 3165 . . . . . . . . 9 (𝑎 ∈ ℝ* → (∃𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤)))
133132reximia 3084 . . . . . . . 8 (∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13494, 133syl 17 . . . . . . 7 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13586, 87, 88, 13419.9d2rf 31400 . . . . . 6 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13671, 72, 81, 135syl21anc 836 . . . . 5 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
137 simprl 769 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → 𝑣𝑋)
138 simprr 771 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → 𝑤𝑌)
13919a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → Fun +𝑒 )
14023adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑋 × 𝑌) ⊆ dom +𝑒 )
141137, 138, 139, 140elovimad 7405 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌)))
1421eleq2d 2823 . . . . . . . . . 10 (𝜑 → ((𝑣 +𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌))))
143142adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → ((𝑣 +𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌))))
144141, 143mpbird 256 . . . . . . . 8 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑣 +𝑒 𝑤) ∈ 𝑍)
145 simpr 485 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝑋𝑤𝑌)) ∧ 𝑘 = (𝑣 +𝑒 𝑤)) → 𝑘 = (𝑣 +𝑒 𝑤))
146145breq2d 5117 . . . . . . . 8 (((𝜑 ∧ (𝑣𝑋𝑤𝑌)) ∧ 𝑘 = (𝑣 +𝑒 𝑤)) → (𝑧 < 𝑘𝑧 < (𝑣 +𝑒 𝑤)))
147144, 146rspcedv 3574 . . . . . . 7 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
148147rexlimdvva 3205 . . . . . 6 (𝜑 → (∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
149148ad2antrr 724 . . . . 5 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → (∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
150136, 149mpd 15 . . . 4 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑘𝑍 𝑧 < 𝑘)
151150ex 413 . . 3 ((𝜑𝑧 ∈ ℝ) → (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))
152151ralrimiva 3143 . 2 (𝜑 → ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))
153 supxr2 13233 . 2 (((𝑍 ⊆ ℝ* ∧ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∈ ℝ*) ∧ (∀𝑧𝑍 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))) → sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
15427, 32, 70, 152, 153syl22anc 837 1 (𝜑 → sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  wss 3910  cop 4592   class class class wbr 5105   × cxp 5631  dom cdm 5633  cima 5636  Fun wfun 6490  wf 6492  cfv 6496  (class class class)co 7357  supcsup 9376  cr 11050  -∞cmnf 11187  *cxr 11188   < clt 11189  cle 11190   +𝑒 cxad 13031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-sup 9378  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-2 12216  df-rp 12916  df-xneg 13033  df-xadd 13034
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator