ixxub

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

	Ref	Expression
Hypotheses	ixx.1	$⊢ O = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x R z \land z S y)\})$
	ixxub.2	$⊢ (w \in ℝ^{} \land B \in ℝ^{}) \to (w < B \to w S B)$
	ixxub.3	$⊢ (w \in ℝ^{} \land B \in ℝ^{}) \to (w S B \to w \leq B)$
	ixxub.4	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A < w \to A R w)$
	ixxub.5	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A R w \to A \leq w)$
Assertion	ixxub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to sup (A O B ℝ^{*} <) = B$

Proof

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

Metamath Proof Explorer

Theorem ixxub

Proof