Metamath Proof Explorer


Theorem 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 ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) = 𝐴 )