# Metamath Proof Explorer

## Theorem supxrun

Description: The supremum of the union of two sets of extended reals equals the largest of their suprema. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion supxrun ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to sup\left({A}\cup {B},{ℝ}^{*},<\right)=sup\left({B},{ℝ}^{*},<\right)$

### Proof

Step Hyp Ref Expression
1 unss ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\right)↔{A}\cup {B}\subseteq {ℝ}^{*}$
2 1 biimpi ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\right)\to {A}\cup {B}\subseteq {ℝ}^{*}$
3 2 3adant3 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to {A}\cup {B}\subseteq {ℝ}^{*}$
4 supxrcl ${⊢}{B}\subseteq {ℝ}^{*}\to sup\left({B},{ℝ}^{*},<\right)\in {ℝ}^{*}$
5 4 3ad2ant2 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to sup\left({B},{ℝ}^{*},<\right)\in {ℝ}^{*}$
6 elun ${⊢}{x}\in \left({A}\cup {B}\right)↔\left({x}\in {A}\vee {x}\in {B}\right)$
7 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
8 7 a1i ${⊢}{A}\subseteq {ℝ}^{*}\to <\mathrm{Or}{ℝ}^{*}$
9 xrsupss ${⊢}{A}\subseteq {ℝ}^{*}\to \exists {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{z}\wedge \forall {z}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({z}<{y}\to \exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{w}\right)\right)$
10 8 9 supub ${⊢}{A}\subseteq {ℝ}^{*}\to \left({x}\in {A}\to ¬sup\left({A},{ℝ}^{*},<\right)<{x}\right)$
11 10 3ad2ant1 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to \left({x}\in {A}\to ¬sup\left({A},{ℝ}^{*},<\right)<{x}\right)$
12 supxrcl ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
13 12 ad2antrr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
14 4 ad2antlr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to sup\left({B},{ℝ}^{*},<\right)\in {ℝ}^{*}$
15 ssel2 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {x}\in {A}\right)\to {x}\in {ℝ}^{*}$
16 15 adantlr ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to {x}\in {ℝ}^{*}$
17 xrlelttr ${⊢}\left(sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge sup\left({B},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\right)\to \left(\left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\wedge sup\left({B},{ℝ}^{*},<\right)<{x}\right)\to sup\left({A},{ℝ}^{*},<\right)<{x}\right)$
18 13 14 16 17 syl3anc ${⊢}\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to \left(\left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\wedge sup\left({B},{ℝ}^{*},<\right)<{x}\right)\to sup\left({A},{ℝ}^{*},<\right)<{x}\right)$
19 18 expdimp ${⊢}\left(\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\right)\wedge {x}\in {A}\right)\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to \left(sup\left({B},{ℝ}^{*},<\right)<{x}\to sup\left({A},{ℝ}^{*},<\right)<{x}\right)$
20 19 con3d ${⊢}\left(\left(\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\right)\wedge {x}\in {A}\right)\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to \left(¬sup\left({A},{ℝ}^{*},<\right)<{x}\to ¬sup\left({B},{ℝ}^{*},<\right)<{x}\right)$
21 20 exp41 ${⊢}{A}\subseteq {ℝ}^{*}\to \left({B}\subseteq {ℝ}^{*}\to \left({x}\in {A}\to \left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\to \left(¬sup\left({A},{ℝ}^{*},<\right)<{x}\to ¬sup\left({B},{ℝ}^{*},<\right)<{x}\right)\right)\right)\right)$
22 21 com34 ${⊢}{A}\subseteq {ℝ}^{*}\to \left({B}\subseteq {ℝ}^{*}\to \left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\to \left({x}\in {A}\to \left(¬sup\left({A},{ℝ}^{*},<\right)<{x}\to ¬sup\left({B},{ℝ}^{*},<\right)<{x}\right)\right)\right)\right)$
23 22 3imp ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to \left({x}\in {A}\to \left(¬sup\left({A},{ℝ}^{*},<\right)<{x}\to ¬sup\left({B},{ℝ}^{*},<\right)<{x}\right)\right)$
24 11 23 mpdd ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to \left({x}\in {A}\to ¬sup\left({B},{ℝ}^{*},<\right)<{x}\right)$
25 7 a1i ${⊢}{B}\subseteq {ℝ}^{*}\to <\mathrm{Or}{ℝ}^{*}$
26 xrsupss ${⊢}{B}\subseteq {ℝ}^{*}\to \exists {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}¬{y}<{z}\wedge \forall {z}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({z}<{y}\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{z}<{w}\right)\right)$
27 25 26 supub ${⊢}{B}\subseteq {ℝ}^{*}\to \left({x}\in {B}\to ¬sup\left({B},{ℝ}^{*},<\right)<{x}\right)$
28 27 3ad2ant2 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to \left({x}\in {B}\to ¬sup\left({B},{ℝ}^{*},<\right)<{x}\right)$
29 24 28 jaod ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to \left(\left({x}\in {A}\vee {x}\in {B}\right)\to ¬sup\left({B},{ℝ}^{*},<\right)<{x}\right)$
30 6 29 syl5bi ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to \left({x}\in \left({A}\cup {B}\right)\to ¬sup\left({B},{ℝ}^{*},<\right)<{x}\right)$
31 30 ralrimiv ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to \forall {x}\in \left({A}\cup {B}\right)\phantom{\rule{.4em}{0ex}}¬sup\left({B},{ℝ}^{*},<\right)<{x}$
32 rexr ${⊢}{x}\in ℝ\to {x}\in {ℝ}^{*}$
33 xrsupss ${⊢}{B}\subseteq {ℝ}^{*}\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}¬{x}<{z}\wedge \forall {z}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({z}<{x}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
34 25 33 suplub ${⊢}{B}\subseteq {ℝ}^{*}\to \left(\left({x}\in {ℝ}^{*}\wedge {x}
35 32 34 sylani ${⊢}{B}\subseteq {ℝ}^{*}\to \left(\left({x}\in ℝ\wedge {x}
36 elun2 ${⊢}{y}\in {B}\to {y}\in \left({A}\cup {B}\right)$
37 36 anim1i ${⊢}\left({y}\in {B}\wedge {x}<{y}\right)\to \left({y}\in \left({A}\cup {B}\right)\wedge {x}<{y}\right)$
38 37 reximi2 ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}<{y}\to \exists {y}\in \left({A}\cup {B}\right)\phantom{\rule{.4em}{0ex}}{x}<{y}$
39 35 38 syl6 ${⊢}{B}\subseteq {ℝ}^{*}\to \left(\left({x}\in ℝ\wedge {x}
40 39 expd ${⊢}{B}\subseteq {ℝ}^{*}\to \left({x}\in ℝ\to \left({x}
41 40 ralrimiv ${⊢}{B}\subseteq {ℝ}^{*}\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}
42 41 3ad2ant2 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}
43 supxr ${⊢}\left(\left({A}\cup {B}\subseteq {ℝ}^{*}\wedge sup\left({B},{ℝ}^{*},<\right)\in {ℝ}^{*}\right)\wedge \left(\forall {x}\in \left({A}\cup {B}\right)\phantom{\rule{.4em}{0ex}}¬sup\left({B},{ℝ}^{*},<\right)<{x}\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x}
44 3 5 31 42 43 syl22anc ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)\right)\to sup\left({A}\cup {B},{ℝ}^{*},<\right)=sup\left({B},{ℝ}^{*},<\right)$