This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infleinf

Description: If any element of B can be approximated from above by members of A , then the infimum of A is less than or equal to the infimum of B . (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses infleinf.a 
|- ( ph -> A C_ RR* )
infleinf.b 
|- ( ph -> B C_ RR* )
infleinf.c 
|- ( ( ph /\ x e. B /\ y e. RR+ ) -> E. z e. A z <_ ( x +e y ) )
Assertion infleinf 
|- ( ph -> inf ( A , RR* , < ) <_ inf ( B , RR* , < ) )

Proof

Step Hyp Ref Expression
1 infleinf.a 
 |-  ( ph -> A C_ RR* )
2 infleinf.b 
 |-  ( ph -> B C_ RR* )
3 infleinf.c 
 |-  ( ( ph /\ x e. B /\ y e. RR+ ) -> E. z e. A z <_ ( x +e y ) )
4 infxrcl 
 |-  ( A C_ RR* -> inf ( A , RR* , < ) e. RR* )
5 1 4 syl 
 |-  ( ph -> inf ( A , RR* , < ) e. RR* )
6 pnfge 
 |-  ( inf ( A , RR* , < ) e. RR* -> inf ( A , RR* , < ) <_ +oo )
7 5 6 syl 
 |-  ( ph -> inf ( A , RR* , < ) <_ +oo )
8 7 adantr 
 |-  ( ( ph /\ B = (/) ) -> inf ( A , RR* , < ) <_ +oo )
9 infeq1 
 |-  ( B = (/) -> inf ( B , RR* , < ) = inf ( (/) , RR* , < ) )
10 xrinf0 
 |-  inf ( (/) , RR* , < ) = +oo
11 10 a1i 
 |-  ( B = (/) -> inf ( (/) , RR* , < ) = +oo )
12 9 11 eqtrd 
 |-  ( B = (/) -> inf ( B , RR* , < ) = +oo )
13 12 eqcomd 
 |-  ( B = (/) -> +oo = inf ( B , RR* , < ) )
14 13 adantl 
 |-  ( ( ph /\ B = (/) ) -> +oo = inf ( B , RR* , < ) )
15 8 14 breqtrd 
 |-  ( ( ph /\ B = (/) ) -> inf ( A , RR* , < ) <_ inf ( B , RR* , < ) )
16 neqne 
 |-  ( -. B = (/) -> B =/= (/) )
17 16 adantl 
 |-  ( ( ph /\ -. B = (/) ) -> B =/= (/) )
18 5 adantr 
 |-  ( ( ph /\ inf ( B , RR* , < ) = -oo ) -> inf ( A , RR* , < ) e. RR* )
19 id 
 |-  ( r e. RR -> r e. RR )
20 2re 
 |-  2 e. RR
21 20 a1i 
 |-  ( r e. RR -> 2 e. RR )
22 19 21 resubcld 
 |-  ( r e. RR -> ( r - 2 ) e. RR )
23 22 adantl 
 |-  ( ( ( ph /\ inf ( B , RR* , < ) = -oo ) /\ r e. RR ) -> ( r - 2 ) e. RR )
24 simpr 
 |-  ( ( ph /\ inf ( B , RR* , < ) = -oo ) -> inf ( B , RR* , < ) = -oo )
25 infxrunb2 
 |-  ( B C_ RR* -> ( A. y e. RR E. x e. B x < y <-> inf ( B , RR* , < ) = -oo ) )
26 2 25 syl 
 |-  ( ph -> ( A. y e. RR E. x e. B x < y <-> inf ( B , RR* , < ) = -oo ) )
27 26 adantr 
 |-  ( ( ph /\ inf ( B , RR* , < ) = -oo ) -> ( A. y e. RR E. x e. B x < y <-> inf ( B , RR* , < ) = -oo ) )
28 24 27 mpbird 
 |-  ( ( ph /\ inf ( B , RR* , < ) = -oo ) -> A. y e. RR E. x e. B x < y )
29 28 adantr 
 |-  ( ( ( ph /\ inf ( B , RR* , < ) = -oo ) /\ r e. RR ) -> A. y e. RR E. x e. B x < y )
30 breq2 
 |-  ( y = ( r - 2 ) -> ( x < y <-> x < ( r - 2 ) ) )
31 30 rexbidv 
 |-  ( y = ( r - 2 ) -> ( E. x e. B x < y <-> E. x e. B x < ( r - 2 ) ) )
32 31 rspcva 
 |-  ( ( ( r - 2 ) e. RR /\ A. y e. RR E. x e. B x < y ) -> E. x e. B x < ( r - 2 ) )
33 23 29 32 syl2anc 
 |-  ( ( ( ph /\ inf ( B , RR* , < ) = -oo ) /\ r e. RR ) -> E. x e. B x < ( r - 2 ) )
34 simpl 
 |-  ( ( ph /\ x e. B ) -> ph )
35 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
36 1rp 
 |-  1 e. RR+
37 36 a1i 
 |-  ( ( ph /\ x e. B ) -> 1 e. RR+ )
38 1ex 
 |-  1 e. _V
39 eleq1 
 |-  ( y = 1 -> ( y e. RR+ <-> 1 e. RR+ ) )
40 39 3anbi3d 
 |-  ( y = 1 -> ( ( ph /\ x e. B /\ y e. RR+ ) <-> ( ph /\ x e. B /\ 1 e. RR+ ) ) )
41 oveq2 
 |-  ( y = 1 -> ( x +e y ) = ( x +e 1 ) )
42 41 breq2d 
 |-  ( y = 1 -> ( z <_ ( x +e y ) <-> z <_ ( x +e 1 ) ) )
43 42 rexbidv 
 |-  ( y = 1 -> ( E. z e. A z <_ ( x +e y ) <-> E. z e. A z <_ ( x +e 1 ) ) )
44 40 43 imbi12d 
 |-  ( y = 1 -> ( ( ( ph /\ x e. B /\ y e. RR+ ) -> E. z e. A z <_ ( x +e y ) ) <-> ( ( ph /\ x e. B /\ 1 e. RR+ ) -> E. z e. A z <_ ( x +e 1 ) ) ) )
45 38 44 3 vtocl 
 |-  ( ( ph /\ x e. B /\ 1 e. RR+ ) -> E. z e. A z <_ ( x +e 1 ) )
46 34 35 37 45 syl3anc 
 |-  ( ( ph /\ x e. B ) -> E. z e. A z <_ ( x +e 1 ) )
47 46 adantlr 
 |-  ( ( ( ph /\ r e. RR ) /\ x e. B ) -> E. z e. A z <_ ( x +e 1 ) )
48 47 3adant3 
 |-  ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) -> E. z e. A z <_ ( x +e 1 ) )
49 simp1l 
 |-  ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) -> ph )
50 49 ad2antrr 
 |-  ( ( ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) /\ z e. A ) /\ z <_ ( x +e 1 ) ) -> ph )
51 50 1 syl 
 |-  ( ( ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) /\ z e. A ) /\ z <_ ( x +e 1 ) ) -> A C_ RR* )
52 50 2 syl 
 |-  ( ( ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) /\ z e. A ) /\ z <_ ( x +e 1 ) ) -> B C_ RR* )
53 simp1r 
 |-  ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) -> r e. RR )
54 53 ad2antrr 
 |-  ( ( ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) /\ z e. A ) /\ z <_ ( x +e 1 ) ) -> r e. RR )
55 simp2 
 |-  ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) -> x e. B )
56 55 ad2antrr 
 |-  ( ( ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) /\ z e. A ) /\ z <_ ( x +e 1 ) ) -> x e. B )
57 simpll3 
 |-  ( ( ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) /\ z e. A ) /\ z <_ ( x +e 1 ) ) -> x < ( r - 2 ) )
58 simplr 
 |-  ( ( ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) /\ z e. A ) /\ z <_ ( x +e 1 ) ) -> z e. A )
59 simpr 
 |-  ( ( ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) /\ z e. A ) /\ z <_ ( x +e 1 ) ) -> z <_ ( x +e 1 ) )
60 51 52 54 56 57 58 59 infleinflem2 
 |-  ( ( ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) /\ z e. A ) /\ z <_ ( x +e 1 ) ) -> z < r )
61 60 ex 
 |-  ( ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) /\ z e. A ) -> ( z <_ ( x +e 1 ) -> z < r ) )
62 61 reximdva 
 |-  ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) -> ( E. z e. A z <_ ( x +e 1 ) -> E. z e. A z < r ) )
63 48 62 mpd 
 |-  ( ( ( ph /\ r e. RR ) /\ x e. B /\ x < ( r - 2 ) ) -> E. z e. A z < r )
64 63 3exp 
 |-  ( ( ph /\ r e. RR ) -> ( x e. B -> ( x < ( r - 2 ) -> E. z e. A z < r ) ) )
65 64 adantlr 
 |-  ( ( ( ph /\ inf ( B , RR* , < ) = -oo ) /\ r e. RR ) -> ( x e. B -> ( x < ( r - 2 ) -> E. z e. A z < r ) ) )
66 65 rexlimdv 
 |-  ( ( ( ph /\ inf ( B , RR* , < ) = -oo ) /\ r e. RR ) -> ( E. x e. B x < ( r - 2 ) -> E. z e. A z < r ) )
67 33 66 mpd 
 |-  ( ( ( ph /\ inf ( B , RR* , < ) = -oo ) /\ r e. RR ) -> E. z e. A z < r )
68 67 ralrimiva 
 |-  ( ( ph /\ inf ( B , RR* , < ) = -oo ) -> A. r e. RR E. z e. A z < r )
69 infxrunb2 
 |-  ( A C_ RR* -> ( A. r e. RR E. z e. A z < r <-> inf ( A , RR* , < ) = -oo ) )
70 1 69 syl 
 |-  ( ph -> ( A. r e. RR E. z e. A z < r <-> inf ( A , RR* , < ) = -oo ) )
71 70 adantr 
 |-  ( ( ph /\ inf ( B , RR* , < ) = -oo ) -> ( A. r e. RR E. z e. A z < r <-> inf ( A , RR* , < ) = -oo ) )
72 68 71 mpbid 
 |-  ( ( ph /\ inf ( B , RR* , < ) = -oo ) -> inf ( A , RR* , < ) = -oo )
73 72 24 eqtr4d 
 |-  ( ( ph /\ inf ( B , RR* , < ) = -oo ) -> inf ( A , RR* , < ) = inf ( B , RR* , < ) )
74 18 73 xreqled 
 |-  ( ( ph /\ inf ( B , RR* , < ) = -oo ) -> inf ( A , RR* , < ) <_ inf ( B , RR* , < ) )
75 74 adantlr 
 |-  ( ( ( ph /\ B =/= (/) ) /\ inf ( B , RR* , < ) = -oo ) -> inf ( A , RR* , < ) <_ inf ( B , RR* , < ) )
76 mnfxr 
 |-  -oo e. RR*
77 76 a1i 
 |-  ( ph -> -oo e. RR* )
78 77 ad2antrr 
 |-  ( ( ( ph /\ B =/= (/) ) /\ -. inf ( B , RR* , < ) = -oo ) -> -oo e. RR* )
79 infxrcl 
 |-  ( B C_ RR* -> inf ( B , RR* , < ) e. RR* )
80 2 79 syl 
 |-  ( ph -> inf ( B , RR* , < ) e. RR* )
81 80 ad2antrr 
 |-  ( ( ( ph /\ B =/= (/) ) /\ -. inf ( B , RR* , < ) = -oo ) -> inf ( B , RR* , < ) e. RR* )
82 mnfle 
 |-  ( inf ( B , RR* , < ) e. RR* -> -oo <_ inf ( B , RR* , < ) )
83 81 82 syl 
 |-  ( ( ( ph /\ B =/= (/) ) /\ -. inf ( B , RR* , < ) = -oo ) -> -oo <_ inf ( B , RR* , < ) )
84 neqne 
 |-  ( -. inf ( B , RR* , < ) = -oo -> inf ( B , RR* , < ) =/= -oo )
85 84 necomd 
 |-  ( -. inf ( B , RR* , < ) = -oo -> -oo =/= inf ( B , RR* , < ) )
86 85 adantl 
 |-  ( ( ( ph /\ B =/= (/) ) /\ -. inf ( B , RR* , < ) = -oo ) -> -oo =/= inf ( B , RR* , < ) )
87 78 81 83 86 xrleneltd 
 |-  ( ( ( ph /\ B =/= (/) ) /\ -. inf ( B , RR* , < ) = -oo ) -> -oo < inf ( B , RR* , < ) )
88 5 ad2antrr 
 |-  ( ( ( ph /\ B =/= (/) ) /\ -oo < inf ( B , RR* , < ) ) -> inf ( A , RR* , < ) e. RR* )
89 80 ad2antrr 
 |-  ( ( ( ph /\ B =/= (/) ) /\ -oo < inf ( B , RR* , < ) ) -> inf ( B , RR* , < ) e. RR* )
90 nfv 
 |-  F/ b ( ( ( ph /\ B =/= (/) ) /\ -oo < inf ( B , RR* , < ) ) /\ w e. RR+ )
91 2 ad3antrrr 
 |-  ( ( ( ( ph /\ B =/= (/) ) /\ -oo < inf ( B , RR* , < ) ) /\ w e. RR+ ) -> B C_ RR* )
92 simpllr 
 |-  ( ( ( ( ph /\ B =/= (/) ) /\ -oo < inf ( B , RR* , < ) ) /\ w e. RR+ ) -> B =/= (/) )
93 simpr 
 |-  ( ( ph /\ -oo < inf ( B , RR* , < ) ) -> -oo < inf ( B , RR* , < ) )
94 infxrbnd2 
 |-  ( B C_ RR* -> ( E. b e. RR A. x e. B b <_ x <-> -oo < inf ( B , RR* , < ) ) )
95 2 94 syl 
 |-  ( ph -> ( E. b e. RR A. x e. B b <_ x <-> -oo < inf ( B , RR* , < ) ) )
96 95 adantr 
 |-  ( ( ph /\ -oo < inf ( B , RR* , < ) ) -> ( E. b e. RR A. x e. B b <_ x <-> -oo < inf ( B , RR* , < ) ) )
97 93 96 mpbird 
 |-  ( ( ph /\ -oo < inf ( B , RR* , < ) ) -> E. b e. RR A. x e. B b <_ x )
98 97 ad4ant13 
 |-  ( ( ( ( ph /\ B =/= (/) ) /\ -oo < inf ( B , RR* , < ) ) /\ w e. RR+ ) -> E. b e. RR A. x e. B b <_ x )
99 simpr 
 |-  ( ( ( ( ph /\ B =/= (/) ) /\ -oo < inf ( B , RR* , < ) ) /\ w e. RR+ ) -> w e. RR+ )
100 99 rphalfcld 
 |-  ( ( ( ( ph /\ B =/= (/) ) /\ -oo < inf ( B , RR* , < ) ) /\ w e. RR+ ) -> ( w / 2 ) e. RR+ )
101 90 91 92 98 100 infrpge 
 |-  ( ( ( ( ph /\ B =/= (/) ) /\ -oo < inf ( B , RR* , < ) ) /\ w e. RR+ ) -> E. x e. B x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) )
102 simpll 
 |-  ( ( ( ph /\ w e. RR+ ) /\ x e. B ) -> ph )
103 simpr 
 |-  ( ( ( ph /\ w e. RR+ ) /\ x e. B ) -> x e. B )
104 rphalfcl 
 |-  ( w e. RR+ -> ( w / 2 ) e. RR+ )
105 104 ad2antlr 
 |-  ( ( ( ph /\ w e. RR+ ) /\ x e. B ) -> ( w / 2 ) e. RR+ )
106 ovex 
 |-  ( w / 2 ) e. _V
107 eleq1 
 |-  ( y = ( w / 2 ) -> ( y e. RR+ <-> ( w / 2 ) e. RR+ ) )
108 107 3anbi3d 
 |-  ( y = ( w / 2 ) -> ( ( ph /\ x e. B /\ y e. RR+ ) <-> ( ph /\ x e. B /\ ( w / 2 ) e. RR+ ) ) )
109 oveq2 
 |-  ( y = ( w / 2 ) -> ( x +e y ) = ( x +e ( w / 2 ) ) )
110 109 breq2d 
 |-  ( y = ( w / 2 ) -> ( z <_ ( x +e y ) <-> z <_ ( x +e ( w / 2 ) ) ) )
111 110 rexbidv 
 |-  ( y = ( w / 2 ) -> ( E. z e. A z <_ ( x +e y ) <-> E. z e. A z <_ ( x +e ( w / 2 ) ) ) )
112 108 111 imbi12d 
 |-  ( y = ( w / 2 ) -> ( ( ( ph /\ x e. B /\ y e. RR+ ) -> E. z e. A z <_ ( x +e y ) ) <-> ( ( ph /\ x e. B /\ ( w / 2 ) e. RR+ ) -> E. z e. A z <_ ( x +e ( w / 2 ) ) ) ) )
113 106 112 3 vtocl 
 |-  ( ( ph /\ x e. B /\ ( w / 2 ) e. RR+ ) -> E. z e. A z <_ ( x +e ( w / 2 ) ) )
114 102 103 105 113 syl3anc 
 |-  ( ( ( ph /\ w e. RR+ ) /\ x e. B ) -> E. z e. A z <_ ( x +e ( w / 2 ) ) )
115 114 3adant3 
 |-  ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) -> E. z e. A z <_ ( x +e ( w / 2 ) ) )
116 simp11l 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) /\ z e. A /\ z <_ ( x +e ( w / 2 ) ) ) -> ph )
117 116 1 syl 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) /\ z e. A /\ z <_ ( x +e ( w / 2 ) ) ) -> A C_ RR* )
118 116 2 syl 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) /\ z e. A /\ z <_ ( x +e ( w / 2 ) ) ) -> B C_ RR* )
119 simp11 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) /\ z e. A /\ z <_ ( x +e ( w / 2 ) ) ) -> ( ph /\ w e. RR+ ) )
120 119 simprd 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) /\ z e. A /\ z <_ ( x +e ( w / 2 ) ) ) -> w e. RR+ )
121 simp12 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) /\ z e. A /\ z <_ ( x +e ( w / 2 ) ) ) -> x e. B )
122 simp3 
 |-  ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) -> x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) )
123 122 3ad2ant1 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) /\ z e. A /\ z <_ ( x +e ( w / 2 ) ) ) -> x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) )
124 simp2 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) /\ z e. A /\ z <_ ( x +e ( w / 2 ) ) ) -> z e. A )
125 simp3 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) /\ z e. A /\ z <_ ( x +e ( w / 2 ) ) ) -> z <_ ( x +e ( w / 2 ) ) )
126 117 118 120 121 123 124 125 infleinflem1 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) /\ z e. A /\ z <_ ( x +e ( w / 2 ) ) ) -> inf ( A , RR* , < ) <_ ( inf ( B , RR* , < ) +e w ) )
127 126 3exp 
 |-  ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) -> ( z e. A -> ( z <_ ( x +e ( w / 2 ) ) -> inf ( A , RR* , < ) <_ ( inf ( B , RR* , < ) +e w ) ) ) )
128 127 rexlimdv 
 |-  ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) -> ( E. z e. A z <_ ( x +e ( w / 2 ) ) -> inf ( A , RR* , < ) <_ ( inf ( B , RR* , < ) +e w ) ) )
129 115 128 mpd 
 |-  ( ( ( ph /\ w e. RR+ ) /\ x e. B /\ x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) ) -> inf ( A , RR* , < ) <_ ( inf ( B , RR* , < ) +e w ) )
130 129 3exp 
 |-  ( ( ph /\ w e. RR+ ) -> ( x e. B -> ( x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) -> inf ( A , RR* , < ) <_ ( inf ( B , RR* , < ) +e w ) ) ) )
131 130 rexlimdv 
 |-  ( ( ph /\ w e. RR+ ) -> ( E. x e. B x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) -> inf ( A , RR* , < ) <_ ( inf ( B , RR* , < ) +e w ) ) )
132 131 ad4ant14 
 |-  ( ( ( ( ph /\ B =/= (/) ) /\ -oo < inf ( B , RR* , < ) ) /\ w e. RR+ ) -> ( E. x e. B x <_ ( inf ( B , RR* , < ) +e ( w / 2 ) ) -> inf ( A , RR* , < ) <_ ( inf ( B , RR* , < ) +e w ) ) )
133 101 132 mpd 
 |-  ( ( ( ( ph /\ B =/= (/) ) /\ -oo < inf ( B , RR* , < ) ) /\ w e. RR+ ) -> inf ( A , RR* , < ) <_ ( inf ( B , RR* , < ) +e w ) )
134 88 89 133 xrlexaddrp 
 |-  ( ( ( ph /\ B =/= (/) ) /\ -oo < inf ( B , RR* , < ) ) -> inf ( A , RR* , < ) <_ inf ( B , RR* , < ) )
135 87 134 syldan 
 |-  ( ( ( ph /\ B =/= (/) ) /\ -. inf ( B , RR* , < ) = -oo ) -> inf ( A , RR* , < ) <_ inf ( B , RR* , < ) )
136 75 135 pm2.61dan 
 |-  ( ( ph /\ B =/= (/) ) -> inf ( A , RR* , < ) <_ inf ( B , RR* , < ) )
137 17 136 syldan 
 |-  ( ( ph /\ -. B = (/) ) -> inf ( A , RR* , < ) <_ inf ( B , RR* , < ) )
138 15 137 pm2.61dan 
 |-  ( ph -> inf ( A , RR* , < ) <_ inf ( B , RR* , < ) )