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 31980
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 3982 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝑋 β†’ π‘₯ ∈ ℝ*))
4 xrofsup.2 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ βŠ† ℝ*)
54sseld 3982 . . . . . . . . 9 (πœ‘ β†’ (𝑦 ∈ π‘Œ β†’ 𝑦 ∈ ℝ*))
63, 5anim12d 610 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ) β†’ (π‘₯ ∈ ℝ* ∧ 𝑦 ∈ ℝ*)))
76imp 408 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ (π‘₯ ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
8 xaddcl 13218 . . . . . . 7 ((π‘₯ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) β†’ (π‘₯ +𝑒 𝑦) ∈ ℝ*)
97, 8syl 17 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ (π‘₯ +𝑒 𝑦) ∈ ℝ*)
109ralrimivva 3201 . . . . 5 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ π‘Œ (π‘₯ +𝑒 𝑦) ∈ ℝ*)
11 fveq2 6892 . . . . . . . 8 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ ( +𝑒 β€˜π‘’) = ( +𝑒 β€˜βŸ¨π‘₯, π‘¦βŸ©))
12 df-ov 7412 . . . . . . . 8 (π‘₯ +𝑒 𝑦) = ( +𝑒 β€˜βŸ¨π‘₯, π‘¦βŸ©)
1311, 12eqtr4di 2791 . . . . . . 7 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ ( +𝑒 β€˜π‘’) = (π‘₯ +𝑒 𝑦))
1413eleq1d 2819 . . . . . 6 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (( +𝑒 β€˜π‘’) ∈ ℝ* ↔ (π‘₯ +𝑒 𝑦) ∈ ℝ*))
1514ralxp 5842 . . . . 5 (βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)( +𝑒 β€˜π‘’) ∈ ℝ* ↔ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ π‘Œ (π‘₯ +𝑒 𝑦) ∈ ℝ*)
1610, 15sylibr 233 . . . 4 (πœ‘ β†’ βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)( +𝑒 β€˜π‘’) ∈ ℝ*)
17 xaddf 13203 . . . . . 6 +𝑒 :(ℝ* Γ— ℝ*)βŸΆβ„*
18 ffun 6721 . . . . . 6 ( +𝑒 :(ℝ* Γ— ℝ*)βŸΆβ„* β†’ Fun +𝑒 )
1917, 18ax-mp 5 . . . . 5 Fun +𝑒
20 xpss12 5692 . . . . . . 7 ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) β†’ (𝑋 Γ— π‘Œ) βŠ† (ℝ* Γ— ℝ*))
212, 4, 20syl2anc 585 . . . . . 6 (πœ‘ β†’ (𝑋 Γ— π‘Œ) βŠ† (ℝ* Γ— ℝ*))
2217fdmi 6730 . . . . . 6 dom +𝑒 = (ℝ* Γ— ℝ*)
2321, 22sseqtrrdi 4034 . . . . 5 (πœ‘ β†’ (𝑋 Γ— π‘Œ) βŠ† dom +𝑒 )
24 funimass4 6957 . . . . 5 ((Fun +𝑒 ∧ (𝑋 Γ— π‘Œ) βŠ† dom +𝑒 ) β†’ (( +𝑒 β€œ (𝑋 Γ— π‘Œ)) βŠ† ℝ* ↔ βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)( +𝑒 β€˜π‘’) ∈ ℝ*))
2519, 23, 24sylancr 588 . . . 4 (πœ‘ β†’ (( +𝑒 β€œ (𝑋 Γ— π‘Œ)) βŠ† ℝ* ↔ βˆ€π‘’ ∈ (𝑋 Γ— π‘Œ)( +𝑒 β€˜π‘’) ∈ ℝ*))
2616, 25mpbird 257 . . 3 (πœ‘ β†’ ( +𝑒 β€œ (𝑋 Γ— π‘Œ)) βŠ† ℝ*)
271, 26eqsstrd 4021 . 2 (πœ‘ β†’ 𝑍 βŠ† ℝ*)
28 supxrcl 13294 . . . 4 (𝑋 βŠ† ℝ* β†’ sup(𝑋, ℝ*, < ) ∈ ℝ*)
292, 28syl 17 . . 3 (πœ‘ β†’ sup(𝑋, ℝ*, < ) ∈ ℝ*)
30 supxrcl 13294 . . . 4 (π‘Œ βŠ† ℝ* β†’ sup(π‘Œ, ℝ*, < ) ∈ ℝ*)
314, 30syl 17 . . 3 (πœ‘ β†’ sup(π‘Œ, ℝ*, < ) ∈ ℝ*)
3229, 31xaddcld 13280 . 2 (πœ‘ β†’ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )) ∈ ℝ*)
331eleq2d 2820 . . . . 5 (πœ‘ β†’ (𝑧 ∈ 𝑍 ↔ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))))
3433pm5.32i 576 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑍) ↔ (πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))))
35 nfvd 1919 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) β†’ β„²π‘₯ 𝑧 ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
36 nfvd 1919 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) β†’ Ⅎ𝑦 𝑧 ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
372ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ 𝑋 βŠ† ℝ*)
38 simprl 770 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ π‘₯ ∈ 𝑋)
39 supxrub 13303 . . . . . . . . . . 11 ((𝑋 βŠ† ℝ* ∧ π‘₯ ∈ 𝑋) β†’ π‘₯ ≀ sup(𝑋, ℝ*, < ))
4037, 38, 39syl2anc 585 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ π‘₯ ≀ sup(𝑋, ℝ*, < ))
414ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ π‘Œ βŠ† ℝ*)
42 simprr 772 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ 𝑦 ∈ π‘Œ)
43 supxrub 13303 . . . . . . . . . . 11 ((π‘Œ βŠ† ℝ* ∧ 𝑦 ∈ π‘Œ) β†’ 𝑦 ≀ sup(π‘Œ, ℝ*, < ))
4441, 42, 43syl2anc 585 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ 𝑦 ≀ sup(π‘Œ, ℝ*, < ))
4537, 38sseldd 3984 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ π‘₯ ∈ ℝ*)
4641, 42sseldd 3984 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ 𝑦 ∈ ℝ*)
4737, 28syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ sup(𝑋, ℝ*, < ) ∈ ℝ*)
4841, 30syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ sup(π‘Œ, ℝ*, < ) ∈ ℝ*)
49 xle2add 13238 . . . . . . . . . . 11 (((π‘₯ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ (sup(𝑋, ℝ*, < ) ∈ ℝ* ∧ sup(π‘Œ, ℝ*, < ) ∈ ℝ*)) β†’ ((π‘₯ ≀ sup(𝑋, ℝ*, < ) ∧ 𝑦 ≀ sup(π‘Œ, ℝ*, < )) β†’ (π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))))
5045, 46, 47, 48, 49syl22anc 838 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ ((π‘₯ ≀ sup(𝑋, ℝ*, < ) ∧ 𝑦 ≀ sup(π‘Œ, ℝ*, < )) β†’ (π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))))
5140, 44, 50mp2and 698 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ (π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
5251ralrimivva 3201 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) β†’ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ π‘Œ (π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
53 fvelima 6958 . . . . . . . . . . 11 ((Fun +𝑒 ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) β†’ βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)( +𝑒 β€˜π‘’) = 𝑧)
5419, 53mpan 689 . . . . . . . . . 10 (𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ)) β†’ βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)( +𝑒 β€˜π‘’) = 𝑧)
5554adantl 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) β†’ βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)( +𝑒 β€˜π‘’) = 𝑧)
5613eqeq1d 2735 . . . . . . . . . 10 (𝑒 = ⟨π‘₯, π‘¦βŸ© β†’ (( +𝑒 β€˜π‘’) = 𝑧 ↔ (π‘₯ +𝑒 𝑦) = 𝑧))
5756rexxp 5843 . . . . . . . . 9 (βˆƒπ‘’ ∈ (𝑋 Γ— π‘Œ)( +𝑒 β€˜π‘’) = 𝑧 ↔ βˆƒπ‘₯ ∈ 𝑋 βˆƒπ‘¦ ∈ π‘Œ (π‘₯ +𝑒 𝑦) = 𝑧)
5855, 57sylib 217 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) β†’ βˆƒπ‘₯ ∈ 𝑋 βˆƒπ‘¦ ∈ π‘Œ (π‘₯ +𝑒 𝑦) = 𝑧)
5952, 58r19.29d2r 3141 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) β†’ βˆƒπ‘₯ ∈ 𝑋 βˆƒπ‘¦ ∈ π‘Œ ((π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )) ∧ (π‘₯ +𝑒 𝑦) = 𝑧))
60 ancom 462 . . . . . . . 8 (((π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )) ∧ (π‘₯ +𝑒 𝑦) = 𝑧) ↔ ((π‘₯ +𝑒 𝑦) = 𝑧 ∧ (π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))))
61602rexbii 3130 . . . . . . 7 (βˆƒπ‘₯ ∈ 𝑋 βˆƒπ‘¦ ∈ π‘Œ ((π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )) ∧ (π‘₯ +𝑒 𝑦) = 𝑧) ↔ βˆƒπ‘₯ ∈ 𝑋 βˆƒπ‘¦ ∈ π‘Œ ((π‘₯ +𝑒 𝑦) = 𝑧 ∧ (π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))))
6259, 61sylib 217 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) β†’ βˆƒπ‘₯ ∈ 𝑋 βˆƒπ‘¦ ∈ π‘Œ ((π‘₯ +𝑒 𝑦) = 𝑧 ∧ (π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))))
63 breq1 5152 . . . . . . . . 9 ((π‘₯ +𝑒 𝑦) = 𝑧 β†’ ((π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )) ↔ 𝑧 ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))))
6463biimpa 478 . . . . . . . 8 (((π‘₯ +𝑒 𝑦) = 𝑧 ∧ (π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ 𝑧 ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
6564reximi 3085 . . . . . . 7 (βˆƒπ‘¦ ∈ π‘Œ ((π‘₯ +𝑒 𝑦) = 𝑧 ∧ (π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ βˆƒπ‘¦ ∈ π‘Œ 𝑧 ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
6665reximi 3085 . . . . . 6 (βˆƒπ‘₯ ∈ 𝑋 βˆƒπ‘¦ ∈ π‘Œ ((π‘₯ +𝑒 𝑦) = 𝑧 ∧ (π‘₯ +𝑒 𝑦) ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ βˆƒπ‘₯ ∈ 𝑋 βˆƒπ‘¦ ∈ π‘Œ 𝑧 ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
6762, 66syl 17 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) β†’ βˆƒπ‘₯ ∈ 𝑋 βˆƒπ‘¦ ∈ π‘Œ 𝑧 ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
6835, 36, 6719.9d2r 31712 . . . 4 ((πœ‘ ∧ 𝑧 ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))) β†’ 𝑧 ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
6934, 68sylbi 216 . . 3 ((πœ‘ ∧ 𝑧 ∈ 𝑍) β†’ 𝑧 ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
7069ralrimiva 3147 . 2 (πœ‘ β†’ βˆ€π‘§ ∈ 𝑍 𝑧 ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
712ad2antrr 725 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ 𝑋 βŠ† ℝ*)
724ad2antrr 725 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ π‘Œ βŠ† ℝ*)
73 simplr 768 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ 𝑧 ∈ ℝ)
7429ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ sup(𝑋, ℝ*, < ) ∈ ℝ*)
7531ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ sup(π‘Œ, ℝ*, < ) ∈ ℝ*)
76 xrofsup.3 . . . . . . . 8 (πœ‘ β†’ sup(𝑋, ℝ*, < ) β‰  -∞)
7776ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ sup(𝑋, ℝ*, < ) β‰  -∞)
78 xrofsup.4 . . . . . . . 8 (πœ‘ β†’ sup(π‘Œ, ℝ*, < ) β‰  -∞)
7978ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ sup(π‘Œ, ℝ*, < ) β‰  -∞)
80 simpr 486 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
8173, 74, 75, 77, 79, 80xlt2addrd 31971 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))
82 nfv 1918 . . . . . . . 8 Ⅎ𝑏(𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*)
83 nfcv 2904 . . . . . . . . 9 Ⅎ𝑏ℝ*
84 nfre1 3283 . . . . . . . . 9 β„²π‘βˆƒπ‘ ∈ ℝ* (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))
8583, 84nfrexw 3311 . . . . . . . 8 β„²π‘βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))
8682, 85nfan 1903 . . . . . . 7 Ⅎ𝑏((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))
87 nfvd 1919 . . . . . . 7 (((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) β†’ β„²π‘Žβˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ 𝑧 < (𝑣 +𝑒 𝑀))
88 nfvd 1919 . . . . . . 7 (((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) β†’ β„²π‘βˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ 𝑧 < (𝑣 +𝑒 𝑀))
89 id 22 . . . . . . . . . . . 12 ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) β†’ (𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*))
9089ralrimivw 3151 . . . . . . . . . . 11 ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) β†’ βˆ€π‘ ∈ ℝ* (𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*))
9190ralrimivw 3151 . . . . . . . . . 10 ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) β†’ βˆ€π‘Ž ∈ ℝ* βˆ€π‘ ∈ ℝ* (𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*))
9291adantr 482 . . . . . . . . 9 (((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) β†’ βˆ€π‘Ž ∈ ℝ* βˆ€π‘ ∈ ℝ* (𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*))
93 simpr 486 . . . . . . . . 9 (((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) β†’ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))
9492, 93r19.29d2r 3141 . . . . . . . 8 (((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) β†’ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))))
95 simplrr 777 . . . . . . . . . . . . . . 15 ((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ (𝑣 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀))) β†’ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))
96953anassrs 1361 . . . . . . . . . . . . . 14 ((((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑀 ∈ π‘Œ) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))
9796simp1d 1143 . . . . . . . . . . . . 13 ((((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑀 ∈ π‘Œ) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ 𝑧 = (π‘Ž +𝑒 𝑏))
98 simp-4l 782 . . . . . . . . . . . . . 14 ((((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑀 ∈ π‘Œ) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ (π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*))
99 simplrl 776 . . . . . . . . . . . . . . . . 17 ((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ (𝑣 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀))) β†’ (𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*))
100993anassrs 1361 . . . . . . . . . . . . . . . 16 ((((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑀 ∈ π‘Œ) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ (𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*))
101100simpld 496 . . . . . . . . . . . . . . 15 ((((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑀 ∈ π‘Œ) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ 𝑋 βŠ† ℝ*)
102 simpllr 775 . . . . . . . . . . . . . . 15 ((((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑀 ∈ π‘Œ) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ 𝑣 ∈ 𝑋)
103101, 102sseldd 3984 . . . . . . . . . . . . . 14 ((((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑀 ∈ π‘Œ) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ 𝑣 ∈ ℝ*)
104100simprd 497 . . . . . . . . . . . . . . 15 ((((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑀 ∈ π‘Œ) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ π‘Œ βŠ† ℝ*)
105 simplr 768 . . . . . . . . . . . . . . 15 ((((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑀 ∈ π‘Œ) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ 𝑀 ∈ π‘Œ)
106104, 105sseldd 3984 . . . . . . . . . . . . . 14 ((((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑀 ∈ π‘Œ) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ 𝑀 ∈ ℝ*)
10798, 103, 106jca32 517 . . . . . . . . . . . . 13 ((((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑀 ∈ π‘Œ) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ ((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ* ∧ 𝑀 ∈ ℝ*)))
108 simpr 486 . . . . . . . . . . . . 13 ((((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑀 ∈ π‘Œ) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀))
109 xlt2add 13239 . . . . . . . . . . . . . . 15 (((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ* ∧ 𝑀 ∈ ℝ*)) β†’ ((π‘Ž < 𝑣 ∧ 𝑏 < 𝑀) β†’ (π‘Ž +𝑒 𝑏) < (𝑣 +𝑒 𝑀)))
110109imp 408 . . . . . . . . . . . . . 14 ((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ* ∧ 𝑀 ∈ ℝ*)) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ (π‘Ž +𝑒 𝑏) < (𝑣 +𝑒 𝑀))
111 breq1 5152 . . . . . . . . . . . . . . 15 (𝑧 = (π‘Ž +𝑒 𝑏) β†’ (𝑧 < (𝑣 +𝑒 𝑀) ↔ (π‘Ž +𝑒 𝑏) < (𝑣 +𝑒 𝑀)))
112111biimpar 479 . . . . . . . . . . . . . 14 ((𝑧 = (π‘Ž +𝑒 𝑏) ∧ (π‘Ž +𝑒 𝑏) < (𝑣 +𝑒 𝑀)) β†’ 𝑧 < (𝑣 +𝑒 𝑀))
113110, 112sylan2 594 . . . . . . . . . . . . 13 ((𝑧 = (π‘Ž +𝑒 𝑏) ∧ (((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ (𝑣 ∈ ℝ* ∧ 𝑀 ∈ ℝ*)) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀))) β†’ 𝑧 < (𝑣 +𝑒 𝑀))
11497, 107, 108, 113syl12anc 836 . . . . . . . . . . . 12 ((((((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) ∧ 𝑣 ∈ 𝑋) ∧ 𝑀 ∈ π‘Œ) ∧ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀)) β†’ 𝑧 < (𝑣 +𝑒 𝑀))
115 simplll 774 . . . . . . . . . . . . . . 15 ((((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) ∧ (π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*)) β†’ 𝑋 βŠ† ℝ*)
116 simprl 770 . . . . . . . . . . . . . . 15 ((((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) ∧ (π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*)) β†’ π‘Ž ∈ ℝ*)
117 simplr2 1217 . . . . . . . . . . . . . . 15 ((((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) ∧ (π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*)) β†’ π‘Ž < sup(𝑋, ℝ*, < ))
118 supxrlub 13304 . . . . . . . . . . . . . . . 16 ((𝑋 βŠ† ℝ* ∧ π‘Ž ∈ ℝ*) β†’ (π‘Ž < sup(𝑋, ℝ*, < ) ↔ βˆƒπ‘£ ∈ 𝑋 π‘Ž < 𝑣))
119118biimpa 478 . . . . . . . . . . . . . . 15 (((𝑋 βŠ† ℝ* ∧ π‘Ž ∈ ℝ*) ∧ π‘Ž < sup(𝑋, ℝ*, < )) β†’ βˆƒπ‘£ ∈ 𝑋 π‘Ž < 𝑣)
120115, 116, 117, 119syl21anc 837 . . . . . . . . . . . . . 14 ((((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) ∧ (π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*)) β†’ βˆƒπ‘£ ∈ 𝑋 π‘Ž < 𝑣)
121 simpllr 775 . . . . . . . . . . . . . . 15 ((((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) ∧ (π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*)) β†’ π‘Œ βŠ† ℝ*)
122 simprr 772 . . . . . . . . . . . . . . 15 ((((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) ∧ (π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*)) β†’ 𝑏 ∈ ℝ*)
123 simplr3 1218 . . . . . . . . . . . . . . 15 ((((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) ∧ (π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*)) β†’ 𝑏 < sup(π‘Œ, ℝ*, < ))
124 supxrlub 13304 . . . . . . . . . . . . . . . 16 ((π‘Œ βŠ† ℝ* ∧ 𝑏 ∈ ℝ*) β†’ (𝑏 < sup(π‘Œ, ℝ*, < ) ↔ βˆƒπ‘€ ∈ π‘Œ 𝑏 < 𝑀))
125124biimpa 478 . . . . . . . . . . . . . . 15 (((π‘Œ βŠ† ℝ* ∧ 𝑏 ∈ ℝ*) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )) β†’ βˆƒπ‘€ ∈ π‘Œ 𝑏 < 𝑀)
126121, 122, 123, 125syl21anc 837 . . . . . . . . . . . . . 14 ((((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) ∧ (π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*)) β†’ βˆƒπ‘€ ∈ π‘Œ 𝑏 < 𝑀)
127 reeanv 3227 . . . . . . . . . . . . . 14 (βˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀) ↔ (βˆƒπ‘£ ∈ 𝑋 π‘Ž < 𝑣 ∧ βˆƒπ‘€ ∈ π‘Œ 𝑏 < 𝑀))
128120, 126, 127sylanbrc 584 . . . . . . . . . . . . 13 ((((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) ∧ (π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*)) β†’ βˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀))
129128ancoms 460 . . . . . . . . . . . 12 (((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) β†’ βˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ (π‘Ž < 𝑣 ∧ 𝑏 < 𝑀))
130114, 129reximddv2 3213 . . . . . . . . . . 11 (((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) ∧ ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < )))) β†’ βˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ 𝑧 < (𝑣 +𝑒 𝑀))
131130ex 414 . . . . . . . . . 10 ((π‘Ž ∈ ℝ* ∧ 𝑏 ∈ ℝ*) β†’ (((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) β†’ βˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ 𝑧 < (𝑣 +𝑒 𝑀)))
132131reximdva 3169 . . . . . . . . 9 (π‘Ž ∈ ℝ* β†’ (βˆƒπ‘ ∈ ℝ* ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) β†’ βˆƒπ‘ ∈ ℝ* βˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ 𝑧 < (𝑣 +𝑒 𝑀)))
133132reximia 3082 . . . . . . . 8 (βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* ((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) β†’ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* βˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ 𝑧 < (𝑣 +𝑒 𝑀))
13494, 133syl 17 . . . . . . 7 (((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) β†’ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* βˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ 𝑧 < (𝑣 +𝑒 𝑀))
13586, 87, 88, 13419.9d2rf 31711 . . . . . 6 (((𝑋 βŠ† ℝ* ∧ π‘Œ βŠ† ℝ*) ∧ βˆƒπ‘Ž ∈ ℝ* βˆƒπ‘ ∈ ℝ* (𝑧 = (π‘Ž +𝑒 𝑏) ∧ π‘Ž < sup(𝑋, ℝ*, < ) ∧ 𝑏 < sup(π‘Œ, ℝ*, < ))) β†’ βˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ 𝑧 < (𝑣 +𝑒 𝑀))
13671, 72, 81, 135syl21anc 837 . . . . 5 (((πœ‘ ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ βˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ 𝑧 < (𝑣 +𝑒 𝑀))
137 simprl 770 . . . . . . . . . 10 ((πœ‘ ∧ (𝑣 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ)) β†’ 𝑣 ∈ 𝑋)
138 simprr 772 . . . . . . . . . 10 ((πœ‘ ∧ (𝑣 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ)) β†’ 𝑀 ∈ π‘Œ)
13919a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ (𝑣 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ)) β†’ Fun +𝑒 )
14023adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ (𝑣 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ)) β†’ (𝑋 Γ— π‘Œ) βŠ† dom +𝑒 )
141137, 138, 139, 140elovimad 7457 . . . . . . . . 9 ((πœ‘ ∧ (𝑣 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ)) β†’ (𝑣 +𝑒 𝑀) ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ)))
1421eleq2d 2820 . . . . . . . . . 10 (πœ‘ β†’ ((𝑣 +𝑒 𝑀) ∈ 𝑍 ↔ (𝑣 +𝑒 𝑀) ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))))
143142adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑣 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ)) β†’ ((𝑣 +𝑒 𝑀) ∈ 𝑍 ↔ (𝑣 +𝑒 𝑀) ∈ ( +𝑒 β€œ (𝑋 Γ— π‘Œ))))
144141, 143mpbird 257 . . . . . . . 8 ((πœ‘ ∧ (𝑣 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ)) β†’ (𝑣 +𝑒 𝑀) ∈ 𝑍)
145 simpr 486 . . . . . . . . 9 (((πœ‘ ∧ (𝑣 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ)) ∧ π‘˜ = (𝑣 +𝑒 𝑀)) β†’ π‘˜ = (𝑣 +𝑒 𝑀))
146145breq2d 5161 . . . . . . . 8 (((πœ‘ ∧ (𝑣 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ)) ∧ π‘˜ = (𝑣 +𝑒 𝑀)) β†’ (𝑧 < π‘˜ ↔ 𝑧 < (𝑣 +𝑒 𝑀)))
147144, 146rspcedv 3606 . . . . . . 7 ((πœ‘ ∧ (𝑣 ∈ 𝑋 ∧ 𝑀 ∈ π‘Œ)) β†’ (𝑧 < (𝑣 +𝑒 𝑀) β†’ βˆƒπ‘˜ ∈ 𝑍 𝑧 < π‘˜))
148147rexlimdvva 3212 . . . . . 6 (πœ‘ β†’ (βˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ 𝑧 < (𝑣 +𝑒 𝑀) β†’ βˆƒπ‘˜ ∈ 𝑍 𝑧 < π‘˜))
149148ad2antrr 725 . . . . 5 (((πœ‘ ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ (βˆƒπ‘£ ∈ 𝑋 βˆƒπ‘€ ∈ π‘Œ 𝑧 < (𝑣 +𝑒 𝑀) β†’ βˆƒπ‘˜ ∈ 𝑍 𝑧 < π‘˜))
150136, 149mpd 15 . . . 4 (((πœ‘ ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < ))) β†’ βˆƒπ‘˜ ∈ 𝑍 𝑧 < π‘˜)
151150ex 414 . . 3 ((πœ‘ ∧ 𝑧 ∈ ℝ) β†’ (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )) β†’ βˆƒπ‘˜ ∈ 𝑍 𝑧 < π‘˜))
152151ralrimiva 3147 . 2 (πœ‘ β†’ βˆ€π‘§ ∈ ℝ (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )) β†’ βˆƒπ‘˜ ∈ 𝑍 𝑧 < π‘˜))
153 supxr2 13293 . 2 (((𝑍 βŠ† ℝ* ∧ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )) ∈ ℝ*) ∧ (βˆ€π‘§ ∈ 𝑍 𝑧 ≀ (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )) ∧ βˆ€π‘§ ∈ ℝ (𝑧 < (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )) β†’ βˆƒπ‘˜ ∈ 𝑍 𝑧 < π‘˜))) β†’ sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
15427, 32, 70, 152, 153syl22anc 838 1 (πœ‘ β†’ sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(π‘Œ, ℝ*, < )))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071   βŠ† wss 3949  βŸ¨cop 4635   class class class wbr 5149   Γ— cxp 5675  dom cdm 5677   β€œ cima 5680  Fun wfun 6538  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409  supcsup 9435  β„cr 11109  -∞cmnf 11246  β„*cxr 11247   < clt 11248   ≀ cle 11249   +𝑒 cxad 13090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-sup 9437  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-2 12275  df-rp 12975  df-xneg 13092  df-xadd 13093
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator