# Metamath Proof Explorer

## Theorem ixxub

Description: Extract the upper bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Hypotheses ixx.1 ${⊢}{O}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{R}{z}\wedge {z}{S}{y}\right)\right\}\right)$
ixxub.2 ${⊢}\left({w}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({w}<{B}\to {w}{S}{B}\right)$
ixxub.3 ${⊢}\left({w}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({w}{S}{B}\to {w}\le {B}\right)$
ixxub.4 ${⊢}\left({A}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left({A}<{w}\to {A}{R}{w}\right)$
ixxub.5 ${⊢}\left({A}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left({A}{R}{w}\to {A}\le {w}\right)$
Assertion ixxub ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to sup\left({A}{O}{B},{ℝ}^{*},<\right)={B}$

### Proof

Step Hyp Ref Expression
1 ixx.1 ${⊢}{O}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{R}{z}\wedge {z}{S}{y}\right)\right\}\right)$
2 ixxub.2 ${⊢}\left({w}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({w}<{B}\to {w}{S}{B}\right)$
3 ixxub.3 ${⊢}\left({w}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({w}{S}{B}\to {w}\le {B}\right)$
4 ixxub.4 ${⊢}\left({A}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left({A}<{w}\to {A}{R}{w}\right)$
5 ixxub.5 ${⊢}\left({A}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left({A}{R}{w}\to {A}\le {w}\right)$
6 1 elixx1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({w}\in \left({A}{O}{B}\right)↔\left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{S}{B}\right)\right)$
7 6 3adant3 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to \left({w}\in \left({A}{O}{B}\right)↔\left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{S}{B}\right)\right)$
8 7 biimpa ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to \left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{S}{B}\right)$
9 8 simp1d ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {w}\in {ℝ}^{*}$
10 9 ex ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to \left({w}\in \left({A}{O}{B}\right)\to {w}\in {ℝ}^{*}\right)$
11 10 ssrdv ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to {A}{O}{B}\subseteq {ℝ}^{*}$
12 supxrcl ${⊢}{A}{O}{B}\subseteq {ℝ}^{*}\to sup\left({A}{O}{B},{ℝ}^{*},<\right)\in {ℝ}^{*}$
13 11 12 syl ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to sup\left({A}{O}{B},{ℝ}^{*},<\right)\in {ℝ}^{*}$
14 simp2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to {B}\in {ℝ}^{*}$
15 8 simp3d ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {w}{S}{B}$
16 14 adantr ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {B}\in {ℝ}^{*}$
17 9 16 3 syl2anc ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to \left({w}{S}{B}\to {w}\le {B}\right)$
18 15 17 mpd ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {w}\le {B}$
19 18 ralrimiva ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to \forall {w}\in \left({A}{O}{B}\right)\phantom{\rule{.4em}{0ex}}{w}\le {B}$
20 supxrleub ${⊢}\left({A}{O}{B}\subseteq {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)\le {B}↔\forall {w}\in \left({A}{O}{B}\right)\phantom{\rule{.4em}{0ex}}{w}\le {B}\right)$
21 11 14 20 syl2anc ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)\le {B}↔\forall {w}\in \left({A}{O}{B}\right)\phantom{\rule{.4em}{0ex}}{w}\le {B}\right)$
22 19 21 mpbird ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to sup\left({A}{O}{B},{ℝ}^{*},<\right)\le {B}$
23 simprl ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}$
24 11 ad2antrr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to {A}{O}{B}\subseteq {ℝ}^{*}$
25 qre ${⊢}{w}\in ℚ\to {w}\in ℝ$
26 25 rexrd ${⊢}{w}\in ℚ\to {w}\in {ℝ}^{*}$
27 26 ad2antlr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to {w}\in {ℝ}^{*}$
28 simp1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to {A}\in {ℝ}^{*}$
29 28 ad2antrr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to {A}\in {ℝ}^{*}$
30 13 ad2antrr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to sup\left({A}{O}{B},{ℝ}^{*},<\right)\in {ℝ}^{*}$
31 simp3 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to {A}{O}{B}\ne \varnothing$
32 n0 ${⊢}{A}{O}{B}\ne \varnothing ↔\exists {w}\phantom{\rule{.4em}{0ex}}{w}\in \left({A}{O}{B}\right)$
33 31 32 sylib ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to \exists {w}\phantom{\rule{.4em}{0ex}}{w}\in \left({A}{O}{B}\right)$
34 28 adantr ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {A}\in {ℝ}^{*}$
35 13 adantr ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to sup\left({A}{O}{B},{ℝ}^{*},<\right)\in {ℝ}^{*}$
36 8 simp2d ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {A}{R}{w}$
37 34 9 5 syl2anc ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to \left({A}{R}{w}\to {A}\le {w}\right)$
38 36 37 mpd ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {A}\le {w}$
39 supxrub ${⊢}\left({A}{O}{B}\subseteq {ℝ}^{*}\wedge {w}\in \left({A}{O}{B}\right)\right)\to {w}\le sup\left({A}{O}{B},{ℝ}^{*},<\right)$
40 11 39 sylan ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {w}\le sup\left({A}{O}{B},{ℝ}^{*},<\right)$
41 34 9 35 38 40 xrletrd ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {A}\le sup\left({A}{O}{B},{ℝ}^{*},<\right)$
42 33 41 exlimddv ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to {A}\le sup\left({A}{O}{B},{ℝ}^{*},<\right)$
43 42 ad2antrr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to {A}\le sup\left({A}{O}{B},{ℝ}^{*},<\right)$
44 29 30 27 43 23 xrlelttrd ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to {A}<{w}$
45 29 27 4 syl2anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to \left({A}<{w}\to {A}{R}{w}\right)$
46 44 45 mpd ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to {A}{R}{w}$
47 simprr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to {w}<{B}$
48 14 ad2antrr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to {B}\in {ℝ}^{*}$
49 27 48 2 syl2anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to \left({w}<{B}\to {w}{S}{B}\right)$
50 47 49 mpd ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to {w}{S}{B}$
51 7 ad2antrr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to \left({w}\in \left({A}{O}{B}\right)↔\left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{S}{B}\right)\right)$
52 27 46 50 51 mpbir3and ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to {w}\in \left({A}{O}{B}\right)$
53 24 52 39 syl2anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to {w}\le sup\left({A}{O}{B},{ℝ}^{*},<\right)$
54 27 30 xrlenltd ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to \left({w}\le sup\left({A}{O}{B},{ℝ}^{*},<\right)↔¬sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\right)$
55 53 54 mpbid ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\wedge \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)\to ¬sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}$
56 23 55 pm2.65da ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\wedge {w}\in ℚ\right)\to ¬\left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)$
57 56 nrexdv ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to ¬\exists {w}\in ℚ\phantom{\rule{.4em}{0ex}}\left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)$
58 qbtwnxr ${⊢}\left(sup\left({A}{O}{B},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge sup\left({A}{O}{B},{ℝ}^{*},<\right)<{B}\right)\to \exists {w}\in ℚ\phantom{\rule{.4em}{0ex}}\left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)$
59 58 3expia ${⊢}\left(sup\left({A}{O}{B},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{B}\to \exists {w}\in ℚ\phantom{\rule{.4em}{0ex}}\left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)$
60 13 14 59 syl2anc ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to \left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{B}\to \exists {w}\in ℚ\phantom{\rule{.4em}{0ex}}\left(sup\left({A}{O}{B},{ℝ}^{*},<\right)<{w}\wedge {w}<{B}\right)\right)$
61 57 60 mtod ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to ¬sup\left({A}{O}{B},{ℝ}^{*},<\right)<{B}$
62 14 13 61 xrnltled ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to {B}\le sup\left({A}{O}{B},{ℝ}^{*},<\right)$
63 13 14 22 62 xrletrid ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}{O}{B}\ne \varnothing \right)\to sup\left({A}{O}{B},{ℝ}^{*},<\right)={B}$