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*,y*z*|xRzzSy
ixxub.2 w*B*w<BwSB
ixxub.3 w*B*wSBwB
ixxub.4 A*w*A<wARw
ixxub.5 A*w*ARwAw
Assertion ixxub A*B*AOBsupAOB*<=B

Proof

Step Hyp Ref Expression
1 ixx.1 O=x*,y*z*|xRzzSy
2 ixxub.2 w*B*w<BwSB
3 ixxub.3 w*B*wSBwB
4 ixxub.4 A*w*A<wARw
5 ixxub.5 A*w*ARwAw
6 1 elixx1 A*B*wAOBw*ARwwSB
7 6 3adant3 A*B*AOBwAOBw*ARwwSB
8 7 biimpa A*B*AOBwAOBw*ARwwSB
9 8 simp1d A*B*AOBwAOBw*
10 9 ex A*B*AOBwAOBw*
11 10 ssrdv A*B*AOBAOB*
12 supxrcl AOB*supAOB*<*
13 11 12 syl A*B*AOBsupAOB*<*
14 simp2 A*B*AOBB*
15 8 simp3d A*B*AOBwAOBwSB
16 14 adantr A*B*AOBwAOBB*
17 9 16 3 syl2anc A*B*AOBwAOBwSBwB
18 15 17 mpd A*B*AOBwAOBwB
19 18 ralrimiva A*B*AOBwAOBwB
20 supxrleub AOB*B*supAOB*<BwAOBwB
21 11 14 20 syl2anc A*B*AOBsupAOB*<BwAOBwB
22 19 21 mpbird A*B*AOBsupAOB*<B
23 simprl A*B*AOBwsupAOB*<<ww<BsupAOB*<<w
24 11 ad2antrr A*B*AOBwsupAOB*<<ww<BAOB*
25 qre ww
26 25 rexrd ww*
27 26 ad2antlr A*B*AOBwsupAOB*<<ww<Bw*
28 simp1 A*B*AOBA*
29 28 ad2antrr A*B*AOBwsupAOB*<<ww<BA*
30 13 ad2antrr A*B*AOBwsupAOB*<<ww<BsupAOB*<*
31 simp3 A*B*AOBAOB
32 n0 AOBwwAOB
33 31 32 sylib A*B*AOBwwAOB
34 28 adantr A*B*AOBwAOBA*
35 13 adantr A*B*AOBwAOBsupAOB*<*
36 8 simp2d A*B*AOBwAOBARw
37 34 9 5 syl2anc A*B*AOBwAOBARwAw
38 36 37 mpd A*B*AOBwAOBAw
39 supxrub AOB*wAOBwsupAOB*<
40 11 39 sylan A*B*AOBwAOBwsupAOB*<
41 34 9 35 38 40 xrletrd A*B*AOBwAOBAsupAOB*<
42 33 41 exlimddv A*B*AOBAsupAOB*<
43 42 ad2antrr A*B*AOBwsupAOB*<<ww<BAsupAOB*<
44 29 30 27 43 23 xrlelttrd A*B*AOBwsupAOB*<<ww<BA<w
45 29 27 4 syl2anc A*B*AOBwsupAOB*<<ww<BA<wARw
46 44 45 mpd A*B*AOBwsupAOB*<<ww<BARw
47 simprr A*B*AOBwsupAOB*<<ww<Bw<B
48 14 ad2antrr A*B*AOBwsupAOB*<<ww<BB*
49 27 48 2 syl2anc A*B*AOBwsupAOB*<<ww<Bw<BwSB
50 47 49 mpd A*B*AOBwsupAOB*<<ww<BwSB
51 7 ad2antrr A*B*AOBwsupAOB*<<ww<BwAOBw*ARwwSB
52 27 46 50 51 mpbir3and A*B*AOBwsupAOB*<<ww<BwAOB
53 24 52 39 syl2anc A*B*AOBwsupAOB*<<ww<BwsupAOB*<
54 27 30 xrlenltd A*B*AOBwsupAOB*<<ww<BwsupAOB*<¬supAOB*<<w
55 53 54 mpbid A*B*AOBwsupAOB*<<ww<B¬supAOB*<<w
56 23 55 pm2.65da A*B*AOBw¬supAOB*<<ww<B
57 56 nrexdv A*B*AOB¬wsupAOB*<<ww<B
58 qbtwnxr supAOB*<*B*supAOB*<<BwsupAOB*<<ww<B
59 58 3expia supAOB*<*B*supAOB*<<BwsupAOB*<<ww<B
60 13 14 59 syl2anc A*B*AOBsupAOB*<<BwsupAOB*<<ww<B
61 57 60 mtod A*B*AOB¬supAOB*<<B
62 14 13 61 xrnltled A*B*AOBBsupAOB*<
63 13 14 22 62 xrletrid A*B*AOBsupAOB*<=B