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

Theorem xrofsup 28923
 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 3567 . . . . . . . . 9 (𝜑 → (𝑥𝑋𝑥 ∈ ℝ*))
4 xrofsup.2 . . . . . . . . . 10 (𝜑𝑌 ⊆ ℝ*)
54sseld 3567 . . . . . . . . 9 (𝜑 → (𝑦𝑌𝑦 ∈ ℝ*))
63, 5anim12d 584 . . . . . . . 8 (𝜑 → ((𝑥𝑋𝑦𝑌) → (𝑥 ∈ ℝ*𝑦 ∈ ℝ*)))
76imp 444 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 ∈ ℝ*𝑦 ∈ ℝ*))
8 xaddcl 11944 . . . . . . 7 ((𝑥 ∈ ℝ*𝑦 ∈ ℝ*) → (𝑥 +𝑒 𝑦) ∈ ℝ*)
97, 8syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 +𝑒 𝑦) ∈ ℝ*)
109ralrimivva 2954 . . . . 5 (𝜑 → ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ∈ ℝ*)
11 fveq2 6103 . . . . . . . 8 (𝑢 = ⟨𝑥, 𝑦⟩ → ( +𝑒𝑢) = ( +𝑒 ‘⟨𝑥, 𝑦⟩))
12 df-ov 6552 . . . . . . . 8 (𝑥 +𝑒 𝑦) = ( +𝑒 ‘⟨𝑥, 𝑦⟩)
1311, 12syl6eqr 2662 . . . . . . 7 (𝑢 = ⟨𝑥, 𝑦⟩ → ( +𝑒𝑢) = (𝑥 +𝑒 𝑦))
1413eleq1d 2672 . . . . . 6 (𝑢 = ⟨𝑥, 𝑦⟩ → (( +𝑒𝑢) ∈ ℝ* ↔ (𝑥 +𝑒 𝑦) ∈ ℝ*))
1514ralxp 5185 . . . . 5 (∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ* ↔ ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ∈ ℝ*)
1610, 15sylibr 223 . . . 4 (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*)
17 xaddf 11929 . . . . . 6 +𝑒 :(ℝ* × ℝ*)⟶ℝ*
18 ffun 5961 . . . . . 6 ( +𝑒 :(ℝ* × ℝ*)⟶ℝ* → Fun +𝑒 )
1917, 18ax-mp 5 . . . . 5 Fun +𝑒
20 xpss12 5148 . . . . . . 7 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → (𝑋 × 𝑌) ⊆ (ℝ* × ℝ*))
212, 4, 20syl2anc 691 . . . . . 6 (𝜑 → (𝑋 × 𝑌) ⊆ (ℝ* × ℝ*))
2217fdmi 5965 . . . . . 6 dom +𝑒 = (ℝ* × ℝ*)
2321, 22syl6sseqr 3615 . . . . 5 (𝜑 → (𝑋 × 𝑌) ⊆ dom +𝑒 )
24 funimass4 6157 . . . . 5 ((Fun +𝑒 ∧ (𝑋 × 𝑌) ⊆ dom +𝑒 ) → (( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*))
2519, 23, 24sylancr 694 . . . 4 (𝜑 → (( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*))
2616, 25mpbird 246 . . 3 (𝜑 → ( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ*)
271, 26eqsstrd 3602 . 2 (𝜑𝑍 ⊆ ℝ*)
28 supxrcl 12017 . . . 4 (𝑋 ⊆ ℝ* → sup(𝑋, ℝ*, < ) ∈ ℝ*)
292, 28syl 17 . . 3 (𝜑 → sup(𝑋, ℝ*, < ) ∈ ℝ*)
30 supxrcl 12017 . . . 4 (𝑌 ⊆ ℝ* → sup(𝑌, ℝ*, < ) ∈ ℝ*)
314, 30syl 17 . . 3 (𝜑 → sup(𝑌, ℝ*, < ) ∈ ℝ*)
3229, 31xaddcld 12003 . 2 (𝜑 → (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∈ ℝ*)
331eleq2d 2673 . . . . 5 (𝜑 → (𝑧𝑍𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))))
3433pm5.32i 667 . . . 4 ((𝜑𝑧𝑍) ↔ (𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))))
35 nfvd 1831 . . . . 5 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑥 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
36 nfvd 1831 . . . . 5 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑦 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
372ad2antrr 758 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑋 ⊆ ℝ*)
38 simprl 790 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
39 supxrub 12026 . . . . . . . . . . 11 ((𝑋 ⊆ ℝ*𝑥𝑋) → 𝑥 ≤ sup(𝑋, ℝ*, < ))
4037, 38, 39syl2anc 691 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥 ≤ sup(𝑋, ℝ*, < ))
414ad2antrr 758 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑌 ⊆ ℝ*)
42 simprr 792 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
43 supxrub 12026 . . . . . . . . . . 11 ((𝑌 ⊆ ℝ*𝑦𝑌) → 𝑦 ≤ sup(𝑌, ℝ*, < ))
4441, 42, 43syl2anc 691 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦 ≤ sup(𝑌, ℝ*, < ))
4537, 38sseldd 3569 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥 ∈ ℝ*)
4641, 42sseldd 3569 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦 ∈ ℝ*)
4737, 28syl 17 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → sup(𝑋, ℝ*, < ) ∈ ℝ*)
4841, 30syl 17 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → sup(𝑌, ℝ*, < ) ∈ ℝ*)
49 xle2add 11961 . . . . . . . . . . 11 (((𝑥 ∈ ℝ*𝑦 ∈ ℝ*) ∧ (sup(𝑋, ℝ*, < ) ∈ ℝ* ∧ sup(𝑌, ℝ*, < ) ∈ ℝ*)) → ((𝑥 ≤ sup(𝑋, ℝ*, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ*, < )) → (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
5045, 46, 47, 48, 49syl22anc 1319 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥 ≤ sup(𝑋, ℝ*, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ*, < )) → (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
5140, 44, 50mp2and 711 . . . . . . . . 9 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
5251ralrimivva 2954 . . . . . . . 8 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
53 fvelima 6158 . . . . . . . . . . 11 ((Fun +𝑒𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5419, 53mpan 702 . . . . . . . . . 10 (𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌)) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5554adantl 481 . . . . . . . . 9 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5613eqeq1d 2612 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (( +𝑒𝑢) = 𝑧 ↔ (𝑥 +𝑒 𝑦) = 𝑧))
5756rexxp 5186 . . . . . . . . 9 (∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧 ↔ ∃𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) = 𝑧)
5855, 57sylib 207 . . . . . . . 8 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) = 𝑧)
5952, 58r19.29d2r 3061 . . . . . . 7 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ (𝑥 +𝑒 𝑦) = 𝑧))
60 ancom 465 . . . . . . . 8 (((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ (𝑥 +𝑒 𝑦) = 𝑧) ↔ ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
61602rexbii 3024 . . . . . . 7 (∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ (𝑥 +𝑒 𝑦) = 𝑧) ↔ ∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
6259, 61sylib 207 . . . . . 6 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
63 breq1 4586 . . . . . . . . 9 ((𝑥 +𝑒 𝑦) = 𝑧 → ((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ↔ 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
6463biimpa 500 . . . . . . . 8 (((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6564reximi 2994 . . . . . . 7 (∃𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6665reximi 2994 . . . . . 6 (∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑥𝑋𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6762, 66syl 17 . . . . 5 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6835, 36, 6719.9d2r 28703 . . . 4 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6934, 68sylbi 206 . . 3 ((𝜑𝑧𝑍) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
7069ralrimiva 2949 . 2 (𝜑 → ∀𝑧𝑍 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
712ad2antrr 758 . . . . . 6 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑋 ⊆ ℝ*)
724ad2antrr 758 . . . . . 6 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑌 ⊆ ℝ*)
73 simplr 788 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑧 ∈ ℝ)
7429ad2antrr 758 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑋, ℝ*, < ) ∈ ℝ*)
7531ad2antrr 758 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑌, ℝ*, < ) ∈ ℝ*)
76 xrofsup.3 . . . . . . . 8 (𝜑 → sup(𝑋, ℝ*, < ) ≠ -∞)
7776ad2antrr 758 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑋, ℝ*, < ) ≠ -∞)
78 xrofsup.4 . . . . . . . 8 (𝜑 → sup(𝑌, ℝ*, < ) ≠ -∞)
7978ad2antrr 758 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑌, ℝ*, < ) ≠ -∞)
80 simpr 476 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
8173, 74, 75, 77, 79, 80xlt2addrd 28913 . . . . . 6 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
82 nfv 1830 . . . . . . . 8 𝑏(𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*)
83 nfcv 2751 . . . . . . . . 9 𝑏*
84 nfre1 2988 . . . . . . . . 9 𝑏𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))
8583, 84nfrex 2990 . . . . . . . 8 𝑏𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))
8682, 85nfan 1816 . . . . . . 7 𝑏((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
87 nfvd 1831 . . . . . . 7 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → Ⅎ𝑎𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
88 nfvd 1831 . . . . . . 7 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → Ⅎ𝑏𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
89 id 22 . . . . . . . . . . . 12 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9089ralrimivw 2950 . . . . . . . . . . 11 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → ∀𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9190ralrimivw 2950 . . . . . . . . . 10 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → ∀𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9291adantr 480 . . . . . . . . 9 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∀𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
93 simpr 476 . . . . . . . . 9 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
9492, 93r19.29d2r 3061 . . . . . . . 8 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))))
95 simplrr 797 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ (𝑣𝑋𝑤𝑌 ∧ (𝑎 < 𝑣𝑏 < 𝑤))) → (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
96953anassrs 1282 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
9796simp1d 1066 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑧 = (𝑎 +𝑒 𝑏))
98 simp-4l 802 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 ∈ ℝ*𝑏 ∈ ℝ*))
99 simplrl 796 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ (𝑣𝑋𝑤𝑌 ∧ (𝑎 < 𝑣𝑏 < 𝑤))) → (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
100993anassrs 1282 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
101100simpld 474 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑋 ⊆ ℝ*)
102 simpllr 795 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑣𝑋)
103101, 102sseldd 3569 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑣 ∈ ℝ*)
104100simprd 478 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑌 ⊆ ℝ*)
105 simplr 788 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑤𝑌)
106104, 105sseldd 3569 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑤 ∈ ℝ*)
10798, 103, 106jca32 556 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)))
108 simpr 476 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 < 𝑣𝑏 < 𝑤))
109 xlt2add 11962 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) → ((𝑎 < 𝑣𝑏 < 𝑤) → (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤)))
110109imp 444 . . . . . . . . . . . . . 14 ((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤))
111 breq1 4586 . . . . . . . . . . . . . . 15 (𝑧 = (𝑎 +𝑒 𝑏) → (𝑧 < (𝑣 +𝑒 𝑤) ↔ (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤)))
112111biimpar 501 . . . . . . . . . . . . . 14 ((𝑧 = (𝑎 +𝑒 𝑏) ∧ (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤)) → 𝑧 < (𝑣 +𝑒 𝑤))
113110, 112sylan2 490 . . . . . . . . . . . . 13 ((𝑧 = (𝑎 +𝑒 𝑏) ∧ (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) ∧ (𝑎 < 𝑣𝑏 < 𝑤))) → 𝑧 < (𝑣 +𝑒 𝑤))
11497, 107, 108, 113syl12anc 1316 . . . . . . . . . . . 12 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑧 < (𝑣 +𝑒 𝑤))
115 simplll 794 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑋 ⊆ ℝ*)
116 simprl 790 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑎 ∈ ℝ*)
117 simplr2 1097 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑎 < sup(𝑋, ℝ*, < ))
118 supxrlub 12027 . . . . . . . . . . . . . . . 16 ((𝑋 ⊆ ℝ*𝑎 ∈ ℝ*) → (𝑎 < sup(𝑋, ℝ*, < ) ↔ ∃𝑣𝑋 𝑎 < 𝑣))
119118biimpa 500 . . . . . . . . . . . . . . 15 (((𝑋 ⊆ ℝ*𝑎 ∈ ℝ*) ∧ 𝑎 < sup(𝑋, ℝ*, < )) → ∃𝑣𝑋 𝑎 < 𝑣)
120115, 116, 117, 119syl21anc 1317 . . . . . . . . . . . . . 14 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑣𝑋 𝑎 < 𝑣)
121 simpllr 795 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑌 ⊆ ℝ*)
122 simprr 792 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑏 ∈ ℝ*)
123 simplr3 1098 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑏 < sup(𝑌, ℝ*, < ))
124 supxrlub 12027 . . . . . . . . . . . . . . . 16 ((𝑌 ⊆ ℝ*𝑏 ∈ ℝ*) → (𝑏 < sup(𝑌, ℝ*, < ) ↔ ∃𝑤𝑌 𝑏 < 𝑤))
125124biimpa 500 . . . . . . . . . . . . . . 15 (((𝑌 ⊆ ℝ*𝑏 ∈ ℝ*) ∧ 𝑏 < sup(𝑌, ℝ*, < )) → ∃𝑤𝑌 𝑏 < 𝑤)
126121, 122, 123, 125syl21anc 1317 . . . . . . . . . . . . . 14 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑤𝑌 𝑏 < 𝑤)
127 reeanv 3086 . . . . . . . . . . . . . 14 (∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤) ↔ (∃𝑣𝑋 𝑎 < 𝑣 ∧ ∃𝑤𝑌 𝑏 < 𝑤))
128120, 126, 127sylanbrc 695 . . . . . . . . . . . . 13 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤))
129128ancoms 468 . . . . . . . . . . . 12 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) → ∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤))
130114, 129reximddv2 3002 . . . . . . . . . . 11 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
131130ex 449 . . . . . . . . . 10 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤)))
132131reximdva 3000 . . . . . . . . 9 (𝑎 ∈ ℝ* → (∃𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤)))
133132reximia 2992 . . . . . . . 8 (∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13494, 133syl 17 . . . . . . 7 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13586, 87, 88, 13419.9d2rf 28702 . . . . . 6 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13671, 72, 81, 135syl21anc 1317 . . . . 5 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
137 simprl 790 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → 𝑣𝑋)
138 simprr 792 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → 𝑤𝑌)
13919a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → Fun +𝑒 )
14023adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑋 × 𝑌) ⊆ dom +𝑒 )
141137, 138, 139, 140elovimad 6591 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌)))
1421eleq2d 2673 . . . . . . . . . 10 (𝜑 → ((𝑣 +𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌))))
143142adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → ((𝑣 +𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌))))
144141, 143mpbird 246 . . . . . . . 8 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑣 +𝑒 𝑤) ∈ 𝑍)
145 simpr 476 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝑋𝑤𝑌)) ∧ 𝑘 = (𝑣 +𝑒 𝑤)) → 𝑘 = (𝑣 +𝑒 𝑤))
146145breq2d 4595 . . . . . . . 8 (((𝜑 ∧ (𝑣𝑋𝑤𝑌)) ∧ 𝑘 = (𝑣 +𝑒 𝑤)) → (𝑧 < 𝑘𝑧 < (𝑣 +𝑒 𝑤)))
147144, 146rspcedv 3286 . . . . . . 7 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
148147rexlimdvva 3020 . . . . . 6 (𝜑 → (∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
149148ad2antrr 758 . . . . 5 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → (∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
150136, 149mpd 15 . . . 4 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑘𝑍 𝑧 < 𝑘)
151150ex 449 . . 3 ((𝜑𝑧 ∈ ℝ) → (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))
152151ralrimiva 2949 . 2 (𝜑 → ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))
153 supxr2 12016 . 2 (((𝑍 ⊆ ℝ* ∧ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∈ ℝ*) ∧ (∀𝑧𝑍 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))) → sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
15427, 32, 70, 152, 153syl22anc 1319 1 (𝜑 → sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540  ⟨cop 4131   class class class wbr 4583   × cxp 5036  dom cdm 5038   “ cima 5041  Fun wfun 5798  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  supcsup 8229  ℝcr 9814  -∞cmnf 9951  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   +𝑒 cxad 11820 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-sup 8231  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-2 10956  df-rp 11709  df-xneg 11822  df-xadd 11823 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator