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 
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )
ixxub.2 
|- ( ( w e. RR* /\ B e. RR* ) -> ( w < B -> w S B ) )
ixxub.3 
|- ( ( w e. RR* /\ B e. RR* ) -> ( w S B -> w <_ B ) )
ixxub.4 
|- ( ( A e. RR* /\ w e. RR* ) -> ( A < w -> A R w ) )
ixxub.5 
|- ( ( A e. RR* /\ w e. RR* ) -> ( A R w -> A <_ w ) )
Assertion ixxlb 
|- ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> inf ( ( A O B ) , RR* , < ) = A )

Proof

Step Hyp Ref Expression
1 ixx.1 
 |-  O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )
2 ixxub.2 
 |-  ( ( w e. RR* /\ B e. RR* ) -> ( w < B -> w S B ) )
3 ixxub.3 
 |-  ( ( w e. RR* /\ B e. RR* ) -> ( w S B -> w <_ B ) )
4 ixxub.4 
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A < w -> A R w ) )
5 ixxub.5 
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A R w -> A <_ w ) )
6 1 elixx1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( w e. ( A O B ) <-> ( w e. RR* /\ A R w /\ w S B ) ) )
7 6 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> ( w e. ( A O B ) <-> ( w e. RR* /\ A R w /\ w S B ) ) )
8 7 biimpa 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> ( w e. RR* /\ A R w /\ w S B ) )
9 8 simp1d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> w e. RR* )
10 9 ex 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> ( w e. ( A O B ) -> w e. RR* ) )
11 10 ssrdv 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> ( A O B ) C_ RR* )
12 infxrcl 
 |-  ( ( A O B ) C_ RR* -> inf ( ( A O B ) , RR* , < ) e. RR* )
13 11 12 syl 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> inf ( ( A O B ) , RR* , < ) e. RR* )
14 simp1 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> A e. RR* )
15 simprr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> w < inf ( ( A O B ) , RR* , < ) )
16 11 ad2antrr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> ( A O B ) C_ RR* )
17 qre 
 |-  ( w e. QQ -> w e. RR )
18 17 rexrd 
 |-  ( w e. QQ -> w e. RR* )
19 18 ad2antlr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> w e. RR* )
20 simprl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> A < w )
21 14 ad2antrr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> A e. RR* )
22 21 19 4 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> ( A < w -> A R w ) )
23 20 22 mpd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> A R w )
24 13 ad2antrr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> inf ( ( A O B ) , RR* , < ) e. RR* )
25 simpll2 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> B e. RR* )
26 simp3 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> ( A O B ) =/= (/) )
27 n0 
 |-  ( ( A O B ) =/= (/) <-> E. w w e. ( A O B ) )
28 26 27 sylib 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> E. w w e. ( A O B ) )
29 13 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> inf ( ( A O B ) , RR* , < ) e. RR* )
30 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> B e. RR* )
31 infxrlb 
 |-  ( ( ( A O B ) C_ RR* /\ w e. ( A O B ) ) -> inf ( ( A O B ) , RR* , < ) <_ w )
32 11 31 sylan 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> inf ( ( A O B ) , RR* , < ) <_ w )
33 8 simp3d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> w S B )
34 9 30 3 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> ( w S B -> w <_ B ) )
35 33 34 mpd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> w <_ B )
36 29 9 30 32 35 xrletrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> inf ( ( A O B ) , RR* , < ) <_ B )
37 28 36 exlimddv 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> inf ( ( A O B ) , RR* , < ) <_ B )
38 37 ad2antrr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> inf ( ( A O B ) , RR* , < ) <_ B )
39 19 24 25 15 38 xrltletrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> w < B )
40 19 25 2 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> ( w < B -> w S B ) )
41 39 40 mpd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> w S B )
42 7 ad2antrr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> ( w e. ( A O B ) <-> ( w e. RR* /\ A R w /\ w S B ) ) )
43 19 23 41 42 mpbir3and 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> w e. ( A O B ) )
44 16 43 31 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> inf ( ( A O B ) , RR* , < ) <_ w )
45 24 19 xrlenltd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> ( inf ( ( A O B ) , RR* , < ) <_ w <-> -. w < inf ( ( A O B ) , RR* , < ) ) )
46 44 45 mpbid 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) -> -. w < inf ( ( A O B ) , RR* , < ) )
47 15 46 pm2.65da 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) -> -. ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) )
48 47 nrexdv 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> -. E. w e. QQ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) )
49 qbtwnxr 
 |-  ( ( A e. RR* /\ inf ( ( A O B ) , RR* , < ) e. RR* /\ A < inf ( ( A O B ) , RR* , < ) ) -> E. w e. QQ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) )
50 49 3expia 
 |-  ( ( A e. RR* /\ inf ( ( A O B ) , RR* , < ) e. RR* ) -> ( A < inf ( ( A O B ) , RR* , < ) -> E. w e. QQ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) )
51 14 13 50 syl2anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> ( A < inf ( ( A O B ) , RR* , < ) -> E. w e. QQ ( A < w /\ w < inf ( ( A O B ) , RR* , < ) ) ) )
52 48 51 mtod 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> -. A < inf ( ( A O B ) , RR* , < ) )
53 13 14 52 xrnltled 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> inf ( ( A O B ) , RR* , < ) <_ A )
54 8 simp2d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> A R w )
55 14 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> A e. RR* )
56 55 9 5 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> ( A R w -> A <_ w ) )
57 54 56 mpd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> A <_ w )
58 57 ralrimiva 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> A. w e. ( A O B ) A <_ w )
59 infxrgelb 
 |-  ( ( ( A O B ) C_ RR* /\ A e. RR* ) -> ( A <_ inf ( ( A O B ) , RR* , < ) <-> A. w e. ( A O B ) A <_ w ) )
60 11 14 59 syl2anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> ( A <_ inf ( ( A O B ) , RR* , < ) <-> A. w e. ( A O B ) A <_ w ) )
61 58 60 mpbird 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> A <_ inf ( ( A O B ) , RR* , < ) )
62 13 14 53 61 xrletrid 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> inf ( ( A O B ) , RR* , < ) = A )