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	⊢ 𝑂 = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
	ixxub.2	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑤 < 𝐵 → 𝑤 𝑆 𝐵 ) )
	ixxub.3	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑤 𝑆 𝐵 → 𝑤 ≤ 𝐵 ) )
	ixxub.4	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) → ( 𝐴 < 𝑤 → 𝐴 𝑅 𝑤 ) )
	ixxub.5	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) → ( 𝐴 𝑅 𝑤 → 𝐴 ≤ 𝑤 ) )
Assertion	ixxlb	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2		ixxub.2	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑤 < 𝐵 → 𝑤 𝑆 𝐵 ) )
3		ixxub.3	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑤 𝑆 𝐵 → 𝑤 ≤ 𝐵 ) )
4		ixxub.4	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) → ( 𝐴 < 𝑤 → 𝐴 𝑅 𝑤 ) )
5		ixxub.5	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) → ( 𝐴 𝑅 𝑤 → 𝐴 ≤ 𝑤 ) )
6	1	elixx1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) )
7	6	3adant3	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) )
8	7	biimpa	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) )
9	8	simp1d	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 ∈ ℝ^* )
10	9	ex	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) → 𝑤 ∈ ℝ^* ) )
11	10	ssrdv	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝐴 𝑂 𝐵 ) ⊆ ℝ^* )
12		infxrcl	⊢ ( ( 𝐴 𝑂 𝐵 ) ⊆ ℝ^* → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ∈ ℝ^* )
13	11 12	syl	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ∈ ℝ^* )
14		simp1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → 𝐴 ∈ ℝ^* )
15		simprr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) )
16	11	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → ( 𝐴 𝑂 𝐵 ) ⊆ ℝ^* )
17		qre	⊢ ( 𝑤 ∈ ℚ → 𝑤 ∈ ℝ )
18	17	rexrd	⊢ ( 𝑤 ∈ ℚ → 𝑤 ∈ ℝ^* )
19	18	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → 𝑤 ∈ ℝ^* )
20		simprl	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → 𝐴 < 𝑤 )
21	14	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → 𝐴 ∈ ℝ^* )
22	21 19 4	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → ( 𝐴 < 𝑤 → 𝐴 𝑅 𝑤 ) )
23	20 22	mpd	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → 𝐴 𝑅 𝑤 )
24	13	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ∈ ℝ^* )
25		simpll2	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → 𝐵 ∈ ℝ^* )
26		simp3	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝐴 𝑂 𝐵 ) ≠ ∅ )
27		n0	⊢ ( ( 𝐴 𝑂 𝐵 ) ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) )
28	26 27	sylib	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ∃ 𝑤 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) )
29	13	adantr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ∈ ℝ^* )
30		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐵 ∈ ℝ^* )
31		infxrlb	⊢ ( ( ( 𝐴 𝑂 𝐵 ) ⊆ ℝ^* ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ≤ 𝑤 )
32	11 31	sylan	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ≤ 𝑤 )
33	8	simp3d	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 𝑆 𝐵 )
34	9 30 3	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → ( 𝑤 𝑆 𝐵 → 𝑤 ≤ 𝐵 ) )
35	33 34	mpd	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 ≤ 𝐵 )
36	29 9 30 32 35	xrletrd	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ≤ 𝐵 )
37	28 36	exlimddv	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ≤ 𝐵 )
38	37	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ≤ 𝐵 )
39	19 24 25 15 38	xrltletrd	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → 𝑤 < 𝐵 )
40	19 25 2	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → ( 𝑤 < 𝐵 → 𝑤 𝑆 𝐵 ) )
41	39 40	mpd	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → 𝑤 𝑆 𝐵 )
42	7	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) )
43	19 23 41 42	mpbir3and	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) )
44	16 43 31	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ≤ 𝑤 )
45	24 19	xrlenltd	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → ( inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ≤ 𝑤 ↔ ¬ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) )
46	44 45	mpbid	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) → ¬ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) )
47	15 46	pm2.65da	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) → ¬ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) )
48	47	nrexdv	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ¬ ∃ 𝑤 ∈ ℚ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) )
49		qbtwnxr	⊢ ( ( 𝐴 ∈ ℝ^* ∧ inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ∈ ℝ^* ∧ 𝐴 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) → ∃ 𝑤 ∈ ℚ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) )
50	49	3expia	⊢ ( ( 𝐴 ∈ ℝ^* ∧ inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ∈ ℝ^* ) → ( 𝐴 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) → ∃ 𝑤 ∈ ℚ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) )
51	14 13 50	syl2anc	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝐴 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) → ∃ 𝑤 ∈ ℚ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ) ) )
52	48 51	mtod	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ¬ 𝐴 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) )
53	13 14 52	xrnltled	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ≤ 𝐴 )
54	8	simp2d	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐴 𝑅 𝑤 )
55	14	adantr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐴 ∈ ℝ^* )
56	55 9 5	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → ( 𝐴 𝑅 𝑤 → 𝐴 ≤ 𝑤 ) )
57	54 56	mpd	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐴 ≤ 𝑤 )
58	57	ralrimiva	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ∀ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) 𝐴 ≤ 𝑤 )
59		infxrgelb	⊢ ( ( ( 𝐴 𝑂 𝐵 ) ⊆ ℝ^* ∧ 𝐴 ∈ ℝ^* ) → ( 𝐴 ≤ inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ↔ ∀ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) 𝐴 ≤ 𝑤 ) )
60	11 14 59	syl2anc	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝐴 ≤ inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) ↔ ∀ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) 𝐴 ≤ 𝑤 ) )
61	58 60	mpbird	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → 𝐴 ≤ inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) )
62	13 14 53 61	xrletrid	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ^* , < ) = 𝐴 )

Metamath Proof Explorer

Theorem ixxlb

Proof