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 31781
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 3968 . . . . . . . . 9 (𝜑 → (𝑥𝑋𝑥 ∈ ℝ*))
4 xrofsup.2 . . . . . . . . . 10 (𝜑𝑌 ⊆ ℝ*)
54sseld 3968 . . . . . . . . 9 (𝜑 → (𝑦𝑌𝑦 ∈ ℝ*))
63, 5anim12d 609 . . . . . . . 8 (𝜑 → ((𝑥𝑋𝑦𝑌) → (𝑥 ∈ ℝ*𝑦 ∈ ℝ*)))
76imp 407 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 ∈ ℝ*𝑦 ∈ ℝ*))
8 xaddcl 13190 . . . . . . 7 ((𝑥 ∈ ℝ*𝑦 ∈ ℝ*) → (𝑥 +𝑒 𝑦) ∈ ℝ*)
97, 8syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 +𝑒 𝑦) ∈ ℝ*)
109ralrimivva 3199 . . . . 5 (𝜑 → ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ∈ ℝ*)
11 fveq2 6869 . . . . . . . 8 (𝑢 = ⟨𝑥, 𝑦⟩ → ( +𝑒𝑢) = ( +𝑒 ‘⟨𝑥, 𝑦⟩))
12 df-ov 7387 . . . . . . . 8 (𝑥 +𝑒 𝑦) = ( +𝑒 ‘⟨𝑥, 𝑦⟩)
1311, 12eqtr4di 2789 . . . . . . 7 (𝑢 = ⟨𝑥, 𝑦⟩ → ( +𝑒𝑢) = (𝑥 +𝑒 𝑦))
1413eleq1d 2817 . . . . . 6 (𝑢 = ⟨𝑥, 𝑦⟩ → (( +𝑒𝑢) ∈ ℝ* ↔ (𝑥 +𝑒 𝑦) ∈ ℝ*))
1514ralxp 5824 . . . . 5 (∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ* ↔ ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ∈ ℝ*)
1610, 15sylibr 233 . . . 4 (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*)
17 xaddf 13175 . . . . . 6 +𝑒 :(ℝ* × ℝ*)⟶ℝ*
18 ffun 6698 . . . . . 6 ( +𝑒 :(ℝ* × ℝ*)⟶ℝ* → Fun +𝑒 )
1917, 18ax-mp 5 . . . . 5 Fun +𝑒
20 xpss12 5675 . . . . . . 7 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → (𝑋 × 𝑌) ⊆ (ℝ* × ℝ*))
212, 4, 20syl2anc 584 . . . . . 6 (𝜑 → (𝑋 × 𝑌) ⊆ (ℝ* × ℝ*))
2217fdmi 6707 . . . . . 6 dom +𝑒 = (ℝ* × ℝ*)
2321, 22sseqtrrdi 4020 . . . . 5 (𝜑 → (𝑋 × 𝑌) ⊆ dom +𝑒 )
24 funimass4 6934 . . . . 5 ((Fun +𝑒 ∧ (𝑋 × 𝑌) ⊆ dom +𝑒 ) → (( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*))
2519, 23, 24sylancr 587 . . . 4 (𝜑 → (( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*))
2616, 25mpbird 256 . . 3 (𝜑 → ( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ*)
271, 26eqsstrd 4007 . 2 (𝜑𝑍 ⊆ ℝ*)
28 supxrcl 13266 . . . 4 (𝑋 ⊆ ℝ* → sup(𝑋, ℝ*, < ) ∈ ℝ*)
292, 28syl 17 . . 3 (𝜑 → sup(𝑋, ℝ*, < ) ∈ ℝ*)
30 supxrcl 13266 . . . 4 (𝑌 ⊆ ℝ* → sup(𝑌, ℝ*, < ) ∈ ℝ*)
314, 30syl 17 . . 3 (𝜑 → sup(𝑌, ℝ*, < ) ∈ ℝ*)
3229, 31xaddcld 13252 . 2 (𝜑 → (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∈ ℝ*)
331eleq2d 2818 . . . . 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 13275 . . . . . . . . . . 11 ((𝑋 ⊆ ℝ*𝑥𝑋) → 𝑥 ≤ sup(𝑋, ℝ*, < ))
4037, 38, 39syl2anc 584 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥 ≤ sup(𝑋, ℝ*, < ))
414ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑌 ⊆ ℝ*)
42 simprr 771 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
43 supxrub 13275 . . . . . . . . . . 11 ((𝑌 ⊆ ℝ*𝑦𝑌) → 𝑦 ≤ sup(𝑌, ℝ*, < ))
4441, 42, 43syl2anc 584 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦 ≤ sup(𝑌, ℝ*, < ))
4537, 38sseldd 3970 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥 ∈ ℝ*)
4641, 42sseldd 3970 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦 ∈ ℝ*)
4737, 28syl 17 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → sup(𝑋, ℝ*, < ) ∈ ℝ*)
4841, 30syl 17 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → sup(𝑌, ℝ*, < ) ∈ ℝ*)
49 xle2add 13210 . . . . . . . . . . 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 3199 . . . . . . . 8 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
53 fvelima 6935 . . . . . . . . . . 11 ((Fun +𝑒𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5419, 53mpan 688 . . . . . . . . . 10 (𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌)) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5554adantl 482 . . . . . . . . 9 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5613eqeq1d 2733 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (( +𝑒𝑢) = 𝑧 ↔ (𝑥 +𝑒 𝑦) = 𝑧))
5756rexxp 5825 . . . . . . . . 9 (∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧 ↔ ∃𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) = 𝑧)
5855, 57sylib 217 . . . . . . . 8 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) = 𝑧)
5952, 58r19.29d2r 3139 . . . . . . 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 5135 . . . . . . . . 9 ((𝑥 +𝑒 𝑦) = 𝑧 → ((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ↔ 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
6463biimpa 477 . . . . . . . 8 (((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6564reximi 3083 . . . . . . 7 (∃𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6665reximi 3083 . . . . . 6 (∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑥𝑋𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6762, 66syl 17 . . . . 5 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6835, 36, 6719.9d2r 31505 . . . 4 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6934, 68sylbi 216 . . 3 ((𝜑𝑧𝑍) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
7069ralrimiva 3145 . 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 31772 . . . . . 6 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
82 nfv 1917 . . . . . . . 8 𝑏(𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*)
83 nfcv 2902 . . . . . . . . 9 𝑏*
84 nfre1 3279 . . . . . . . . 9 𝑏𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))
8583, 84nfrexw 3307 . . . . . . . 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 3149 . . . . . . . . . . 11 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → ∀𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9190ralrimivw 3149 . . . . . . . . . 10 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → ∀𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9291adantr 481 . . . . . . . . 9 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∀𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
93 simpr 485 . . . . . . . . 9 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
9492, 93r19.29d2r 3139 . . . . . . . 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 3970 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑣 ∈ ℝ*)
104100simprd 496 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑌 ⊆ ℝ*)
105 simplr 767 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑤𝑌)
106104, 105sseldd 3970 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑤 ∈ ℝ*)
10798, 103, 106jca32 516 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)))
108 simpr 485 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 < 𝑣𝑏 < 𝑤))
109 xlt2add 13211 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) → ((𝑎 < 𝑣𝑏 < 𝑤) → (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤)))
110109imp 407 . . . . . . . . . . . . . 14 ((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤))
111 breq1 5135 . . . . . . . . . . . . . . 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 13276 . . . . . . . . . . . . . . . 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 13276 . . . . . . . . . . . . . . . 16 ((𝑌 ⊆ ℝ*𝑏 ∈ ℝ*) → (𝑏 < sup(𝑌, ℝ*, < ) ↔ ∃𝑤𝑌 𝑏 < 𝑤))
125124biimpa 477 . . . . . . . . . . . . . . 15 (((𝑌 ⊆ ℝ*𝑏 ∈ ℝ*) ∧ 𝑏 < sup(𝑌, ℝ*, < )) → ∃𝑤𝑌 𝑏 < 𝑤)
126121, 122, 123, 125syl21anc 836 . . . . . . . . . . . . . 14 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑤𝑌 𝑏 < 𝑤)
127 reeanv 3225 . . . . . . . . . . . . . 14 (∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤) ↔ (∃𝑣𝑋 𝑎 < 𝑣 ∧ ∃𝑤𝑌 𝑏 < 𝑤))
128120, 126, 127sylanbrc 583 . . . . . . . . . . . . 13 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤))
129128ancoms 459 . . . . . . . . . . . 12 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) → ∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤))
130114, 129reximddv2 3211 . . . . . . . . . . 11 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
131130ex 413 . . . . . . . . . 10 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤)))
132131reximdva 3167 . . . . . . . . 9 (𝑎 ∈ ℝ* → (∃𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤)))
133132reximia 3080 . . . . . . . 8 (∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13494, 133syl 17 . . . . . . 7 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13586, 87, 88, 13419.9d2rf 31504 . . . . . 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 7432 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌)))
1421eleq2d 2818 . . . . . . . . . 10 (𝜑 → ((𝑣 +𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌))))
143142adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → ((𝑣 +𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌))))
144141, 143mpbird 256 . . . . . . . 8 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑣 +𝑒 𝑤) ∈ 𝑍)
145 simpr 485 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝑋𝑤𝑌)) ∧ 𝑘 = (𝑣 +𝑒 𝑤)) → 𝑘 = (𝑣 +𝑒 𝑤))
146145breq2d 5144 . . . . . . . 8 (((𝜑 ∧ (𝑣𝑋𝑤𝑌)) ∧ 𝑘 = (𝑣 +𝑒 𝑤)) → (𝑧 < 𝑘𝑧 < (𝑣 +𝑒 𝑤)))
147144, 146rspcedv 3595 . . . . . . 7 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
148147rexlimdvva 3210 . . . . . 6 (𝜑 → (∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
149148ad2antrr 724 . . . . 5 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → (∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
150136, 149mpd 15 . . . 4 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑘𝑍 𝑧 < 𝑘)
151150ex 413 . . 3 ((𝜑𝑧 ∈ ℝ) → (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))
152151ralrimiva 3145 . 2 (𝜑 → ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))
153 supxr2 13265 . 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 2939  wral 3060  wrex 3069  wss 3935  cop 4619   class class class wbr 5132   × cxp 5658  dom cdm 5660  cima 5663  Fun wfun 6517  wf 6519  cfv 6523  (class class class)co 7384  supcsup 9407  cr 11081  -∞cmnf 11218  *cxr 11219   < clt 11220  cle 11221   +𝑒 cxad 13062
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 2702  ax-sep 5283  ax-nul 5290  ax-pow 5347  ax-pr 5411  ax-un 7699  ax-cnex 11138  ax-resscn 11139  ax-1cn 11140  ax-icn 11141  ax-addcl 11142  ax-addrcl 11143  ax-mulcl 11144  ax-mulrcl 11145  ax-mulcom 11146  ax-addass 11147  ax-mulass 11148  ax-distr 11149  ax-i2m1 11150  ax-1ne0 11151  ax-1rid 11152  ax-rnegex 11153  ax-rrecex 11154  ax-cnre 11155  ax-pre-lttri 11156  ax-pre-lttrn 11157  ax-pre-ltadd 11158  ax-pre-mulgt0 11159  ax-pre-sup 11160
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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3371  df-reu 3372  df-rab 3426  df-v 3468  df-sbc 3765  df-csb 3881  df-dif 3938  df-un 3940  df-in 3942  df-ss 3952  df-nul 4310  df-if 4514  df-pw 4589  df-sn 4614  df-pr 4616  df-op 4620  df-uni 4893  df-iun 4983  df-br 5133  df-opab 5195  df-mpt 5216  df-id 5558  df-po 5572  df-so 5573  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6475  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7340  df-ov 7387  df-oprab 7388  df-mpo 7389  df-1st 7948  df-2nd 7949  df-er 8677  df-en 8913  df-dom 8914  df-sdom 8915  df-sup 9409  df-pnf 11222  df-mnf 11223  df-xr 11224  df-ltxr 11225  df-le 11226  df-sub 11418  df-neg 11419  df-div 11844  df-2 12247  df-rp 12947  df-xneg 13064  df-xadd 13065
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator