ixxlb

Description: Extract the lower bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014) (Revised by AV, 12-Sep-2020)

	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	ixxlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to inf (A O B ℝ^{*} <) = A$

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		infxrcl	$⊢ A O B \subseteq ℝ^{} \to inf (A O B ℝ^{} <) \in ℝ^{*}$
13	11 12	syl	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to inf (A O B ℝ^{} <) \in ℝ^{}$
14		simp1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to A \in ℝ^{*}$
15		simprr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{} <))) \to w < inf (A O B ℝ^{} <)$
16	11	ad2antrr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{} <))) \to A O B \subseteq ℝ^{}$
17		qre	$⊢ w \in ℚ \to w \in ℝ$
18	17	rexrd	$⊢ w \in ℚ \to w \in ℝ^{*}$
19	18	ad2antlr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{} <))) \to w \in ℝ^{}$
20		simprl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{*} <))) \to A < w$
21	14	ad2antrr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{} <))) \to A \in ℝ^{}$
22	21 19 4	syl2anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{*} <))) \to (A < w \to A R w)$
23	20 22	mpd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{*} <))) \to A R w$
24	13	ad2antrr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{} <))) \to inf (A O B ℝ^{} <) \in ℝ^{*}$
25		simpll2	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{} <))) \to B \in ℝ^{}$
26		simp3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to A O B \neq \emptyset$
27		n0	$⊢ A O B \neq \emptyset \leftrightarrow \exists w w \in (A O B)$
28	26 27	sylib	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to \exists w w \in (A O B)$
29	13	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in (A O B)) \to inf (A O B ℝ^{} <) \in ℝ^{}$
30		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in (A O B)) \to B \in ℝ^{*}$
31		infxrlb	$⊢ (A O B \subseteq ℝ^{} \land w \in (A O B)) \to inf (A O B ℝ^{} <) \leq w$
32	11 31	sylan	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in (A O B)) \to inf (A O B ℝ^{*} <) \leq w$
33	8	simp3d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in (A O B)) \to w S B$
34	9 30 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)$
35	33 34	mpd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in (A O B)) \to w \leq B$
36	29 9 30 32 35	xrletrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in (A O B)) \to inf (A O B ℝ^{*} <) \leq B$
37	28 36	exlimddv	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to inf (A O B ℝ^{*} <) \leq B$
38	37	ad2antrr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{} <))) \to inf (A O B ℝ^{} <) \leq B$
39	19 24 25 15 38	xrltletrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{*} <))) \to w < B$
40	19 25 2	syl2anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{*} <))) \to (w < B \to w S B)$
41	39 40	mpd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{*} <))) \to w S B$
42	7	ad2antrr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{} <))) \to (w \in (A O B) \leftrightarrow (w \in ℝ^{} \land A R w \land w S B))$
43	19 23 41 42	mpbir3and	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{*} <))) \to w \in (A O B)$
44	16 43 31	syl2anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{} <))) \to inf (A O B ℝ^{} <) \leq w$
45	24 19	xrlenltd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{} <))) \to (inf (A O B ℝ^{} <) \leq w \leftrightarrow \neg w < inf (A O B ℝ^{*} <))$
46	44 45	mpbid	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \land (A < w \land w < inf (A O B ℝ^{} <))) \to \neg w < inf (A O B ℝ^{} <)$
47	15 46	pm2.65da	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in ℚ) \to \neg (A < w \land w < inf (A O B ℝ^{*} <))$
48	47	nrexdv	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to \neg \exists w \in ℚ (A < w \land w < inf (A O B ℝ^{*} <))$
49		qbtwnxr	$⊢ (A \in ℝ^{} \land inf (A O B ℝ^{} <) \in ℝ^{} \land A < inf (A O B ℝ^{} <)) \to \exists w \in ℚ (A < w \land w < inf (A O B ℝ^{*} <))$
50	49	3expia	$⊢ (A \in ℝ^{} \land inf (A O B ℝ^{} <) \in ℝ^{}) \to (A < inf (A O B ℝ^{} <) \to \exists w \in ℚ (A < w \land w < inf (A O B ℝ^{*} <)))$
51	14 13 50	syl2anc	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to (A < inf (A O B ℝ^{} <) \to \exists w \in ℚ (A < w \land w < inf (A O B ℝ^{} <)))$
52	48 51	mtod	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to \neg A < inf (A O B ℝ^{*} <)$
53	13 14 52	xrnltled	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to inf (A O B ℝ^{*} <) \leq A$
54	8	simp2d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in (A O B)) \to A R w$
55	14	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in (A O B)) \to A \in ℝ^{*}$
56	55 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)$
57	54 56	mpd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \land w \in (A O B)) \to A \leq w$
58	57	ralrimiva	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to \forall w \in (A O B) A \leq w$
59		infxrgelb	$⊢ (A O B \subseteq ℝ^{} \land A \in ℝ^{}) \to (A \leq inf (A O B ℝ^{*} <) \leftrightarrow \forall w \in (A O B) A \leq w)$
60	11 14 59	syl2anc	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to (A \leq inf (A O B ℝ^{*} <) \leftrightarrow \forall w \in (A O B) A \leq w)$
61	58 60	mpbird	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to A \leq inf (A O B ℝ^{*} <)$
62	13 14 53 61	xrletrid	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A O B \neq \emptyset) \to inf (A O B ℝ^{*} <) = A$

Metamath Proof Explorer

Theorem ixxlb

Proof