Metamath Proof Explorer

Theorem ixxub

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

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 ixxub 
|- ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> sup ( ( A O B ) , RR* , < ) = B )

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 supxrcl 
 |-  ( ( A O B ) C_ RR* -> sup ( ( A O B ) , RR* , < ) e. RR* )
13 11 12 syl 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> sup ( ( A O B ) , RR* , < ) e. RR* )
14 simp2 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> B e. RR* )
15 8 simp3d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> w S B )
16 14 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> B e. RR* )
17 9 16 3 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> ( w S B -> w <_ B ) )
18 15 17 mpd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> w <_ B )
19 18 ralrimiva 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> A. w e. ( A O B ) w <_ B )
20 supxrleub 
 |-  ( ( ( A O B ) C_ RR* /\ B e. RR* ) -> ( sup ( ( A O B ) , RR* , < ) <_ B <-> A. w e. ( A O B ) w <_ B ) )
21 11 14 20 syl2anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> ( sup ( ( A O B ) , RR* , < ) <_ B <-> A. w e. ( A O B ) w <_ B ) )
22 19 21 mpbird 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> sup ( ( A O B ) , RR* , < ) <_ B )
23 simprl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> sup ( ( A O B ) , RR* , < ) < w )
24 11 ad2antrr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> ( A O B ) C_ RR* )
25 qre 
 |-  ( w e. QQ -> w e. RR )
26 25 rexrd 
 |-  ( w e. QQ -> w e. RR* )
27 26 ad2antlr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> w e. RR* )
28 simp1 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> A e. RR* )
29 28 ad2antrr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> A e. RR* )
30 13 ad2antrr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> sup ( ( A O B ) , RR* , < ) e. RR* )
31 simp3 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> ( A O B ) =/= (/) )
32 n0 
 |-  ( ( A O B ) =/= (/) <-> E. w w e. ( A O B ) )
33 31 32 sylib 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> E. w w e. ( A O B ) )
34 28 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> A e. RR* )
35 13 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> sup ( ( A O B ) , RR* , < ) e. RR* )
36 8 simp2d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> A R w )
37 34 9 5 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> ( A R w -> A <_ w ) )
38 36 37 mpd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> A <_ w )
39 supxrub 
 |-  ( ( ( A O B ) C_ RR* /\ w e. ( A O B ) ) -> w <_ sup ( ( A O B ) , RR* , < ) )
40 11 39 sylan 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> w <_ sup ( ( A O B ) , RR* , < ) )
41 34 9 35 38 40 xrletrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. ( A O B ) ) -> A <_ sup ( ( A O B ) , RR* , < ) )
42 33 41 exlimddv 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> A <_ sup ( ( A O B ) , RR* , < ) )
43 42 ad2antrr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> A <_ sup ( ( A O B ) , RR* , < ) )
44 29 30 27 43 23 xrlelttrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> A < w )
45 29 27 4 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> ( A < w -> A R w ) )
46 44 45 mpd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> A R w )
47 simprr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> w < B )
48 14 ad2antrr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> B e. RR* )
49 27 48 2 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> ( w < B -> w S B ) )
50 47 49 mpd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> w S B )
51 7 ad2antrr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> ( w e. ( A O B ) <-> ( w e. RR* /\ A R w /\ w S B ) ) )
52 27 46 50 51 mpbir3and 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> w e. ( A O B ) )
53 24 52 39 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> w <_ sup ( ( A O B ) , RR* , < ) )
54 27 30 xrlenltd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> ( w <_ sup ( ( A O B ) , RR* , < ) <-> -. sup ( ( A O B ) , RR* , < ) < w ) )
55 53 54 mpbid 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) /\ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) -> -. sup ( ( A O B ) , RR* , < ) < w )
56 23 55 pm2.65da 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) /\ w e. QQ ) -> -. ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) )
57 56 nrexdv 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> -. E. w e. QQ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) )
58 qbtwnxr 
 |-  ( ( sup ( ( A O B ) , RR* , < ) e. RR* /\ B e. RR* /\ sup ( ( A O B ) , RR* , < ) < B ) -> E. w e. QQ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) )
59 58 3expia 
 |-  ( ( sup ( ( A O B ) , RR* , < ) e. RR* /\ B e. RR* ) -> ( sup ( ( A O B ) , RR* , < ) < B -> E. w e. QQ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) )
60 13 14 59 syl2anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> ( sup ( ( A O B ) , RR* , < ) < B -> E. w e. QQ ( sup ( ( A O B ) , RR* , < ) < w /\ w < B ) ) )
61 57 60 mtod 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> -. sup ( ( A O B ) , RR* , < ) < B )
62 14 13 61 xrnltled 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> B <_ sup ( ( A O B ) , RR* , < ) )
63 13 14 22 62 xrletrid 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A O B ) =/= (/) ) -> sup ( ( A O B ) , RR* , < ) = B )