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 30098
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 3819 . . . . . . . . 9 (𝜑 → (𝑥𝑋𝑥 ∈ ℝ*))
4 xrofsup.2 . . . . . . . . . 10 (𝜑𝑌 ⊆ ℝ*)
54sseld 3819 . . . . . . . . 9 (𝜑 → (𝑦𝑌𝑦 ∈ ℝ*))
63, 5anim12d 602 . . . . . . . 8 (𝜑 → ((𝑥𝑋𝑦𝑌) → (𝑥 ∈ ℝ*𝑦 ∈ ℝ*)))
76imp 397 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 ∈ ℝ*𝑦 ∈ ℝ*))
8 xaddcl 12382 . . . . . . 7 ((𝑥 ∈ ℝ*𝑦 ∈ ℝ*) → (𝑥 +𝑒 𝑦) ∈ ℝ*)
97, 8syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 +𝑒 𝑦) ∈ ℝ*)
109ralrimivva 3152 . . . . 5 (𝜑 → ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ∈ ℝ*)
11 fveq2 6446 . . . . . . . 8 (𝑢 = ⟨𝑥, 𝑦⟩ → ( +𝑒𝑢) = ( +𝑒 ‘⟨𝑥, 𝑦⟩))
12 df-ov 6925 . . . . . . . 8 (𝑥 +𝑒 𝑦) = ( +𝑒 ‘⟨𝑥, 𝑦⟩)
1311, 12syl6eqr 2831 . . . . . . 7 (𝑢 = ⟨𝑥, 𝑦⟩ → ( +𝑒𝑢) = (𝑥 +𝑒 𝑦))
1413eleq1d 2843 . . . . . 6 (𝑢 = ⟨𝑥, 𝑦⟩ → (( +𝑒𝑢) ∈ ℝ* ↔ (𝑥 +𝑒 𝑦) ∈ ℝ*))
1514ralxp 5509 . . . . 5 (∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ* ↔ ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ∈ ℝ*)
1610, 15sylibr 226 . . . 4 (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*)
17 xaddf 12367 . . . . . 6 +𝑒 :(ℝ* × ℝ*)⟶ℝ*
18 ffun 6294 . . . . . 6 ( +𝑒 :(ℝ* × ℝ*)⟶ℝ* → Fun +𝑒 )
1917, 18ax-mp 5 . . . . 5 Fun +𝑒
20 xpss12 5370 . . . . . . 7 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → (𝑋 × 𝑌) ⊆ (ℝ* × ℝ*))
212, 4, 20syl2anc 579 . . . . . 6 (𝜑 → (𝑋 × 𝑌) ⊆ (ℝ* × ℝ*))
2217fdmi 6301 . . . . . 6 dom +𝑒 = (ℝ* × ℝ*)
2321, 22syl6sseqr 3870 . . . . 5 (𝜑 → (𝑋 × 𝑌) ⊆ dom +𝑒 )
24 funimass4 6507 . . . . 5 ((Fun +𝑒 ∧ (𝑋 × 𝑌) ⊆ dom +𝑒 ) → (( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*))
2519, 23, 24sylancr 581 . . . 4 (𝜑 → (( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ* ↔ ∀𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) ∈ ℝ*))
2616, 25mpbird 249 . . 3 (𝜑 → ( +𝑒 “ (𝑋 × 𝑌)) ⊆ ℝ*)
271, 26eqsstrd 3857 . 2 (𝜑𝑍 ⊆ ℝ*)
28 supxrcl 12457 . . . 4 (𝑋 ⊆ ℝ* → sup(𝑋, ℝ*, < ) ∈ ℝ*)
292, 28syl 17 . . 3 (𝜑 → sup(𝑋, ℝ*, < ) ∈ ℝ*)
30 supxrcl 12457 . . . 4 (𝑌 ⊆ ℝ* → sup(𝑌, ℝ*, < ) ∈ ℝ*)
314, 30syl 17 . . 3 (𝜑 → sup(𝑌, ℝ*, < ) ∈ ℝ*)
3229, 31xaddcld 12443 . 2 (𝜑 → (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∈ ℝ*)
331eleq2d 2844 . . . . 5 (𝜑 → (𝑧𝑍𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))))
3433pm5.32i 570 . . . 4 ((𝜑𝑧𝑍) ↔ (𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))))
35 nfvd 1958 . . . . 5 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑥 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
36 nfvd 1958 . . . . 5 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → Ⅎ𝑦 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
372ad2antrr 716 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑋 ⊆ ℝ*)
38 simprl 761 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
39 supxrub 12466 . . . . . . . . . . 11 ((𝑋 ⊆ ℝ*𝑥𝑋) → 𝑥 ≤ sup(𝑋, ℝ*, < ))
4037, 38, 39syl2anc 579 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥 ≤ sup(𝑋, ℝ*, < ))
414ad2antrr 716 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑌 ⊆ ℝ*)
42 simprr 763 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
43 supxrub 12466 . . . . . . . . . . 11 ((𝑌 ⊆ ℝ*𝑦𝑌) → 𝑦 ≤ sup(𝑌, ℝ*, < ))
4441, 42, 43syl2anc 579 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦 ≤ sup(𝑌, ℝ*, < ))
4537, 38sseldd 3821 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥 ∈ ℝ*)
4641, 42sseldd 3821 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦 ∈ ℝ*)
4737, 28syl 17 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → sup(𝑋, ℝ*, < ) ∈ ℝ*)
4841, 30syl 17 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → sup(𝑌, ℝ*, < ) ∈ ℝ*)
49 xle2add 12401 . . . . . . . . . . 11 (((𝑥 ∈ ℝ*𝑦 ∈ ℝ*) ∧ (sup(𝑋, ℝ*, < ) ∈ ℝ* ∧ sup(𝑌, ℝ*, < ) ∈ ℝ*)) → ((𝑥 ≤ sup(𝑋, ℝ*, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ*, < )) → (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
5045, 46, 47, 48, 49syl22anc 829 . . . . . . . . . 10 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥 ≤ sup(𝑋, ℝ*, < ) ∧ 𝑦 ≤ sup(𝑌, ℝ*, < )) → (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
5140, 44, 50mp2and 689 . . . . . . . . 9 (((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
5251ralrimivva 3152 . . . . . . . 8 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∀𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
53 fvelima 6508 . . . . . . . . . . 11 ((Fun +𝑒𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5419, 53mpan 680 . . . . . . . . . 10 (𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌)) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5554adantl 475 . . . . . . . . 9 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧)
5613eqeq1d 2779 . . . . . . . . . 10 (𝑢 = ⟨𝑥, 𝑦⟩ → (( +𝑒𝑢) = 𝑧 ↔ (𝑥 +𝑒 𝑦) = 𝑧))
5756rexxp 5510 . . . . . . . . 9 (∃𝑢 ∈ (𝑋 × 𝑌)( +𝑒𝑢) = 𝑧 ↔ ∃𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) = 𝑧)
5855, 57sylib 210 . . . . . . . 8 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 (𝑥 +𝑒 𝑦) = 𝑧)
5952, 58r19.29d2r 3265 . . . . . . 7 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ (𝑥 +𝑒 𝑦) = 𝑧))
60 ancom 454 . . . . . . . 8 (((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ (𝑥 +𝑒 𝑦) = 𝑧) ↔ ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
61602rexbii 3224 . . . . . . 7 (∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ (𝑥 +𝑒 𝑦) = 𝑧) ↔ ∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
6259, 61sylib 210 . . . . . 6 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
63 breq1 4889 . . . . . . . . 9 ((𝑥 +𝑒 𝑦) = 𝑧 → ((𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ↔ 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))))
6463biimpa 470 . . . . . . . 8 (((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6564reximi 3191 . . . . . . 7 (∃𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6665reximi 3191 . . . . . 6 (∃𝑥𝑋𝑦𝑌 ((𝑥 +𝑒 𝑦) = 𝑧 ∧ (𝑥 +𝑒 𝑦) ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑥𝑋𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6762, 66syl 17 . . . . 5 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → ∃𝑥𝑋𝑦𝑌 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6835, 36, 6719.9d2r 29891 . . . 4 ((𝜑𝑧 ∈ ( +𝑒 “ (𝑋 × 𝑌))) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
6934, 68sylbi 209 . . 3 ((𝜑𝑧𝑍) → 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
7069ralrimiva 3147 . 2 (𝜑 → ∀𝑧𝑍 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
712ad2antrr 716 . . . . . 6 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑋 ⊆ ℝ*)
724ad2antrr 716 . . . . . 6 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑌 ⊆ ℝ*)
73 simplr 759 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑧 ∈ ℝ)
7429ad2antrr 716 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑋, ℝ*, < ) ∈ ℝ*)
7531ad2antrr 716 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑌, ℝ*, < ) ∈ ℝ*)
76 xrofsup.3 . . . . . . . 8 (𝜑 → sup(𝑋, ℝ*, < ) ≠ -∞)
7776ad2antrr 716 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑋, ℝ*, < ) ≠ -∞)
78 xrofsup.4 . . . . . . . 8 (𝜑 → sup(𝑌, ℝ*, < ) ≠ -∞)
7978ad2antrr 716 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → sup(𝑌, ℝ*, < ) ≠ -∞)
80 simpr 479 . . . . . . 7 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
8173, 74, 75, 77, 79, 80xlt2addrd 30088 . . . . . 6 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
82 nfv 1957 . . . . . . . 8 𝑏(𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*)
83 nfcv 2933 . . . . . . . . 9 𝑏*
84 nfre1 3185 . . . . . . . . 9 𝑏𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))
8583, 84nfrex 3187 . . . . . . . 8 𝑏𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))
8682, 85nfan 1946 . . . . . . 7 𝑏((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
87 nfvd 1958 . . . . . . 7 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → Ⅎ𝑎𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
88 nfvd 1958 . . . . . . 7 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → Ⅎ𝑏𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
89 id 22 . . . . . . . . . . . 12 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9089ralrimivw 3148 . . . . . . . . . . 11 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → ∀𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9190ralrimivw 3148 . . . . . . . . . 10 ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) → ∀𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
9291adantr 474 . . . . . . . . 9 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∀𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
93 simpr 479 . . . . . . . . 9 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
9492, 93r19.29d2r 3265 . . . . . . . 8 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))))
95 simplrr 768 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ (𝑣𝑋𝑤𝑌 ∧ (𝑎 < 𝑣𝑏 < 𝑤))) → (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
96953anassrs 1422 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))
9796simp1d 1133 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑧 = (𝑎 +𝑒 𝑏))
98 simp-4l 773 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 ∈ ℝ*𝑏 ∈ ℝ*))
99 simplrl 767 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ (𝑣𝑋𝑤𝑌 ∧ (𝑎 < 𝑣𝑏 < 𝑤))) → (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
100993anassrs 1422 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*))
101100simpld 490 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑋 ⊆ ℝ*)
102 simpllr 766 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑣𝑋)
103101, 102sseldd 3821 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑣 ∈ ℝ*)
104100simprd 491 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑌 ⊆ ℝ*)
105 simplr 759 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑤𝑌)
106104, 105sseldd 3821 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑤 ∈ ℝ*)
10798, 103, 106jca32 511 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)))
108 simpr 479 . . . . . . . . . . . . 13 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 < 𝑣𝑏 < 𝑤))
109 xlt2add 12402 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) → ((𝑎 < 𝑣𝑏 < 𝑤) → (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤)))
110109imp 397 . . . . . . . . . . . . . 14 ((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤))
111 breq1 4889 . . . . . . . . . . . . . . 15 (𝑧 = (𝑎 +𝑒 𝑏) → (𝑧 < (𝑣 +𝑒 𝑤) ↔ (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤)))
112111biimpar 471 . . . . . . . . . . . . . 14 ((𝑧 = (𝑎 +𝑒 𝑏) ∧ (𝑎 +𝑒 𝑏) < (𝑣 +𝑒 𝑤)) → 𝑧 < (𝑣 +𝑒 𝑤))
113110, 112sylan2 586 . . . . . . . . . . . . 13 ((𝑧 = (𝑎 +𝑒 𝑏) ∧ (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ*𝑤 ∈ ℝ*)) ∧ (𝑎 < 𝑣𝑏 < 𝑤))) → 𝑧 < (𝑣 +𝑒 𝑤))
11497, 107, 108, 113syl12anc 827 . . . . . . . . . . . 12 ((((((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) ∧ 𝑣𝑋) ∧ 𝑤𝑌) ∧ (𝑎 < 𝑣𝑏 < 𝑤)) → 𝑧 < (𝑣 +𝑒 𝑤))
115 simplll 765 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑋 ⊆ ℝ*)
116 simprl 761 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑎 ∈ ℝ*)
117 simplr2 1234 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑎 < sup(𝑋, ℝ*, < ))
118 supxrlub 12467 . . . . . . . . . . . . . . . 16 ((𝑋 ⊆ ℝ*𝑎 ∈ ℝ*) → (𝑎 < sup(𝑋, ℝ*, < ) ↔ ∃𝑣𝑋 𝑎 < 𝑣))
119118biimpa 470 . . . . . . . . . . . . . . 15 (((𝑋 ⊆ ℝ*𝑎 ∈ ℝ*) ∧ 𝑎 < sup(𝑋, ℝ*, < )) → ∃𝑣𝑋 𝑎 < 𝑣)
120115, 116, 117, 119syl21anc 828 . . . . . . . . . . . . . 14 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑣𝑋 𝑎 < 𝑣)
121 simpllr 766 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑌 ⊆ ℝ*)
122 simprr 763 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑏 ∈ ℝ*)
123 simplr3 1236 . . . . . . . . . . . . . . 15 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → 𝑏 < sup(𝑌, ℝ*, < ))
124 supxrlub 12467 . . . . . . . . . . . . . . . 16 ((𝑌 ⊆ ℝ*𝑏 ∈ ℝ*) → (𝑏 < sup(𝑌, ℝ*, < ) ↔ ∃𝑤𝑌 𝑏 < 𝑤))
125124biimpa 470 . . . . . . . . . . . . . . 15 (((𝑌 ⊆ ℝ*𝑏 ∈ ℝ*) ∧ 𝑏 < sup(𝑌, ℝ*, < )) → ∃𝑤𝑌 𝑏 < 𝑤)
126121, 122, 123, 125syl21anc 828 . . . . . . . . . . . . . 14 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑤𝑌 𝑏 < 𝑤)
127 reeanv 3292 . . . . . . . . . . . . . 14 (∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤) ↔ (∃𝑣𝑋 𝑎 < 𝑣 ∧ ∃𝑤𝑌 𝑏 < 𝑤))
128120, 126, 127sylanbrc 578 . . . . . . . . . . . . 13 ((((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) ∧ (𝑎 ∈ ℝ*𝑏 ∈ ℝ*)) → ∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤))
129128ancoms 452 . . . . . . . . . . . 12 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) → ∃𝑣𝑋𝑤𝑌 (𝑎 < 𝑣𝑏 < 𝑤))
130114, 129reximddv2 3201 . . . . . . . . . . 11 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < )))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
131130ex 403 . . . . . . . . . 10 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤)))
132131reximdva 3197 . . . . . . . . 9 (𝑎 ∈ ℝ* → (∃𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤)))
133132reximia 3189 . . . . . . . 8 (∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* ((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13494, 133syl 17 . . . . . . 7 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13586, 87, 88, 13419.9d2rf 29890 . . . . . 6 (((𝑋 ⊆ ℝ*𝑌 ⊆ ℝ*) ∧ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* (𝑧 = (𝑎 +𝑒 𝑏) ∧ 𝑎 < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(𝑌, ℝ*, < ))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
13671, 72, 81, 135syl21anc 828 . . . . 5 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤))
137 simprl 761 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → 𝑣𝑋)
138 simprr 763 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → 𝑤𝑌)
13919a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → Fun +𝑒 )
14023adantr 474 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑋 × 𝑌) ⊆ dom +𝑒 )
141137, 138, 139, 140elovimad 6969 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌)))
1421eleq2d 2844 . . . . . . . . . 10 (𝜑 → ((𝑣 +𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌))))
143142adantr 474 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → ((𝑣 +𝑒 𝑤) ∈ 𝑍 ↔ (𝑣 +𝑒 𝑤) ∈ ( +𝑒 “ (𝑋 × 𝑌))))
144141, 143mpbird 249 . . . . . . . 8 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑣 +𝑒 𝑤) ∈ 𝑍)
145 simpr 479 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝑋𝑤𝑌)) ∧ 𝑘 = (𝑣 +𝑒 𝑤)) → 𝑘 = (𝑣 +𝑒 𝑤))
146145breq2d 4898 . . . . . . . 8 (((𝜑 ∧ (𝑣𝑋𝑤𝑌)) ∧ 𝑘 = (𝑣 +𝑒 𝑤)) → (𝑧 < 𝑘𝑧 < (𝑣 +𝑒 𝑤)))
147144, 146rspcedv 3514 . . . . . . 7 ((𝜑 ∧ (𝑣𝑋𝑤𝑌)) → (𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
148147rexlimdvva 3220 . . . . . 6 (𝜑 → (∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
149148ad2antrr 716 . . . . 5 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → (∃𝑣𝑋𝑤𝑌 𝑧 < (𝑣 +𝑒 𝑤) → ∃𝑘𝑍 𝑧 < 𝑘))
150136, 149mpd 15 . . . 4 (((𝜑𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) → ∃𝑘𝑍 𝑧 < 𝑘)
151150ex 403 . . 3 ((𝜑𝑧 ∈ ℝ) → (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))
152151ralrimiva 3147 . 2 (𝜑 → ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))
153 supxr2 12456 . 2 (((𝑍 ⊆ ℝ* ∧ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∈ ℝ*) ∧ (∀𝑧𝑍 𝑧 ≤ (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) ∧ ∀𝑧 ∈ ℝ (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )) → ∃𝑘𝑍 𝑧 < 𝑘))) → sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
15427, 32, 70, 152, 153syl22anc 829 1 (𝜑 → sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wcel 2106  wne 2968  wral 3089  wrex 3090  wss 3791  cop 4403   class class class wbr 4886   × cxp 5353  dom cdm 5355  cima 5358  Fun wfun 6129  wf 6131  cfv 6135  (class class class)co 6922  supcsup 8634  cr 10271  -∞cmnf 10409  *cxr 10410   < clt 10411  cle 10412   +𝑒 cxad 12255
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-po 5274  df-so 5275  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-1st 7445  df-2nd 7446  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-sup 8636  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-2 11438  df-rp 12138  df-xneg 12257  df-xadd 12258
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator