Metamath Proof Explorer


Theorem infxr

Description: The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses infxr.x
|- F/ x ph
infxr.y
|- F/ y ph
infxr.a
|- ( ph -> A C_ RR* )
infxr.b
|- ( ph -> B e. RR* )
infxr.n
|- ( ph -> A. x e. A -. x < B )
infxr.e
|- ( ph -> A. x e. RR ( B < x -> E. y e. A y < x ) )
Assertion infxr
|- ( ph -> inf ( A , RR* , < ) = B )

Proof

Step Hyp Ref Expression
1 infxr.x
 |-  F/ x ph
2 infxr.y
 |-  F/ y ph
3 infxr.a
 |-  ( ph -> A C_ RR* )
4 infxr.b
 |-  ( ph -> B e. RR* )
5 infxr.n
 |-  ( ph -> A. x e. A -. x < B )
6 infxr.e
 |-  ( ph -> A. x e. RR ( B < x -> E. y e. A y < x ) )
7 6 r19.21bi
 |-  ( ( ph /\ x e. RR ) -> ( B < x -> E. y e. A y < x ) )
8 7 adantlr
 |-  ( ( ( ph /\ x e. RR* ) /\ x e. RR ) -> ( B < x -> E. y e. A y < x ) )
9 simplll
 |-  ( ( ( ( ph /\ x e. RR* ) /\ -. x e. RR ) /\ B < x ) -> ph )
10 simpllr
 |-  ( ( ( ( ph /\ x e. RR* ) /\ -. x e. RR ) /\ B < x ) -> x e. RR* )
11 simplr
 |-  ( ( ( ( ph /\ x e. RR* ) /\ -. x e. RR ) /\ B < x ) -> -. x e. RR )
12 mnfxr
 |-  -oo e. RR*
13 12 a1i
 |-  ( ( ( ph /\ x e. RR* ) /\ B < x ) -> -oo e. RR* )
14 simplr
 |-  ( ( ( ph /\ x e. RR* ) /\ B < x ) -> x e. RR* )
15 4 ad2antrr
 |-  ( ( ( ph /\ x e. RR* ) /\ B < x ) -> B e. RR* )
16 mnfle
 |-  ( B e. RR* -> -oo <_ B )
17 4 16 syl
 |-  ( ph -> -oo <_ B )
18 17 ad2antrr
 |-  ( ( ( ph /\ x e. RR* ) /\ B < x ) -> -oo <_ B )
19 simpr
 |-  ( ( ( ph /\ x e. RR* ) /\ B < x ) -> B < x )
20 13 15 14 18 19 xrlelttrd
 |-  ( ( ( ph /\ x e. RR* ) /\ B < x ) -> -oo < x )
21 13 14 20 xrgtned
 |-  ( ( ( ph /\ x e. RR* ) /\ B < x ) -> x =/= -oo )
22 21 adantlr
 |-  ( ( ( ( ph /\ x e. RR* ) /\ -. x e. RR ) /\ B < x ) -> x =/= -oo )
23 10 11 22 xrnmnfpnf
 |-  ( ( ( ( ph /\ x e. RR* ) /\ -. x e. RR ) /\ B < x ) -> x = +oo )
24 simpr
 |-  ( ( ( ( ph /\ x e. RR* ) /\ -. x e. RR ) /\ B < x ) -> B < x )
25 simpl
 |-  ( ( ph /\ B = -oo ) -> ph )
26 id
 |-  ( B = -oo -> B = -oo )
27 1re
 |-  1 e. RR
28 mnflt
 |-  ( 1 e. RR -> -oo < 1 )
29 27 28 ax-mp
 |-  -oo < 1
30 26 29 eqbrtrdi
 |-  ( B = -oo -> B < 1 )
31 30 adantl
 |-  ( ( ph /\ B = -oo ) -> B < 1 )
32 1red
 |-  ( ph -> 1 e. RR )
33 breq2
 |-  ( x = 1 -> ( B < x <-> B < 1 ) )
34 breq2
 |-  ( x = 1 -> ( y < x <-> y < 1 ) )
35 34 rexbidv
 |-  ( x = 1 -> ( E. y e. A y < x <-> E. y e. A y < 1 ) )
36 33 35 imbi12d
 |-  ( x = 1 -> ( ( B < x -> E. y e. A y < x ) <-> ( B < 1 -> E. y e. A y < 1 ) ) )
37 36 rspcva
 |-  ( ( 1 e. RR /\ A. x e. RR ( B < x -> E. y e. A y < x ) ) -> ( B < 1 -> E. y e. A y < 1 ) )
38 32 6 37 syl2anc
 |-  ( ph -> ( B < 1 -> E. y e. A y < 1 ) )
39 25 31 38 sylc
 |-  ( ( ph /\ B = -oo ) -> E. y e. A y < 1 )
40 39 adantlr
 |-  ( ( ( ph /\ x = +oo ) /\ B = -oo ) -> E. y e. A y < 1 )
41 nfv
 |-  F/ y x = +oo
42 2 41 nfan
 |-  F/ y ( ph /\ x = +oo )
43 3 sselda
 |-  ( ( ph /\ y e. A ) -> y e. RR* )
44 43 ad4ant13
 |-  ( ( ( ( ph /\ x = +oo ) /\ y e. A ) /\ y < 1 ) -> y e. RR* )
45 1xr
 |-  1 e. RR*
46 45 a1i
 |-  ( ( ( ( ph /\ x = +oo ) /\ y e. A ) /\ y < 1 ) -> 1 e. RR* )
47 id
 |-  ( x = +oo -> x = +oo )
48 pnfxr
 |-  +oo e. RR*
49 47 48 eqeltrdi
 |-  ( x = +oo -> x e. RR* )
50 49 adantl
 |-  ( ( ph /\ x = +oo ) -> x e. RR* )
51 50 ad2antrr
 |-  ( ( ( ( ph /\ x = +oo ) /\ y e. A ) /\ y < 1 ) -> x e. RR* )
52 simpr
 |-  ( ( ( ( ph /\ x = +oo ) /\ y e. A ) /\ y < 1 ) -> y < 1 )
53 ltpnf
 |-  ( 1 e. RR -> 1 < +oo )
54 27 53 ax-mp
 |-  1 < +oo
55 54 a1i
 |-  ( x = +oo -> 1 < +oo )
56 47 eqcomd
 |-  ( x = +oo -> +oo = x )
57 55 56 breqtrd
 |-  ( x = +oo -> 1 < x )
58 57 adantl
 |-  ( ( ph /\ x = +oo ) -> 1 < x )
59 58 ad2antrr
 |-  ( ( ( ( ph /\ x = +oo ) /\ y e. A ) /\ y < 1 ) -> 1 < x )
60 44 46 51 52 59 xrlttrd
 |-  ( ( ( ( ph /\ x = +oo ) /\ y e. A ) /\ y < 1 ) -> y < x )
61 60 ex
 |-  ( ( ( ph /\ x = +oo ) /\ y e. A ) -> ( y < 1 -> y < x ) )
62 61 ex
 |-  ( ( ph /\ x = +oo ) -> ( y e. A -> ( y < 1 -> y < x ) ) )
63 42 62 reximdai
 |-  ( ( ph /\ x = +oo ) -> ( E. y e. A y < 1 -> E. y e. A y < x ) )
64 63 adantr
 |-  ( ( ( ph /\ x = +oo ) /\ B = -oo ) -> ( E. y e. A y < 1 -> E. y e. A y < x ) )
65 40 64 mpd
 |-  ( ( ( ph /\ x = +oo ) /\ B = -oo ) -> E. y e. A y < x )
66 65 3adantl3
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ B = -oo ) -> E. y e. A y < x )
67 4 adantr
 |-  ( ( ph /\ -. B = -oo ) -> B e. RR* )
68 67 3ad2antl1
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> B e. RR* )
69 26 necon3bi
 |-  ( -. B = -oo -> B =/= -oo )
70 69 adantl
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> B =/= -oo )
71 48 a1i
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> +oo e. RR* )
72 simpr
 |-  ( ( x = +oo /\ B < x ) -> B < x )
73 simpl
 |-  ( ( x = +oo /\ B < x ) -> x = +oo )
74 72 73 breqtrd
 |-  ( ( x = +oo /\ B < x ) -> B < +oo )
75 74 3adant1
 |-  ( ( ph /\ x = +oo /\ B < x ) -> B < +oo )
76 75 adantr
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> B < +oo )
77 68 71 76 xrltned
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> B =/= +oo )
78 68 70 77 xrred
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> B e. RR )
79 27 a1i
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> 1 e. RR )
80 78 79 readdcld
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> ( B + 1 ) e. RR )
81 6 adantr
 |-  ( ( ph /\ -. B = -oo ) -> A. x e. RR ( B < x -> E. y e. A y < x ) )
82 81 3ad2antl1
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> A. x e. RR ( B < x -> E. y e. A y < x ) )
83 80 82 jca
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> ( ( B + 1 ) e. RR /\ A. x e. RR ( B < x -> E. y e. A y < x ) ) )
84 78 ltp1d
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> B < ( B + 1 ) )
85 breq2
 |-  ( x = ( B + 1 ) -> ( B < x <-> B < ( B + 1 ) ) )
86 breq2
 |-  ( x = ( B + 1 ) -> ( y < x <-> y < ( B + 1 ) ) )
87 86 rexbidv
 |-  ( x = ( B + 1 ) -> ( E. y e. A y < x <-> E. y e. A y < ( B + 1 ) ) )
88 85 87 imbi12d
 |-  ( x = ( B + 1 ) -> ( ( B < x -> E. y e. A y < x ) <-> ( B < ( B + 1 ) -> E. y e. A y < ( B + 1 ) ) ) )
89 88 rspcva
 |-  ( ( ( B + 1 ) e. RR /\ A. x e. RR ( B < x -> E. y e. A y < x ) ) -> ( B < ( B + 1 ) -> E. y e. A y < ( B + 1 ) ) )
90 83 84 89 sylc
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> E. y e. A y < ( B + 1 ) )
91 nfv
 |-  F/ y B < x
92 2 41 91 nf3an
 |-  F/ y ( ph /\ x = +oo /\ B < x )
93 nfv
 |-  F/ y -. B = -oo
94 92 93 nfan
 |-  F/ y ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo )
95 43 3ad2antl1
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ y e. A ) -> y e. RR* )
96 95 ad4ant13
 |-  ( ( ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) /\ y e. A ) /\ y < ( B + 1 ) ) -> y e. RR* )
97 80 adantr
 |-  ( ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) /\ y e. A ) -> ( B + 1 ) e. RR )
98 97 rexrd
 |-  ( ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) /\ y e. A ) -> ( B + 1 ) e. RR* )
99 98 adantr
 |-  ( ( ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) /\ y e. A ) /\ y < ( B + 1 ) ) -> ( B + 1 ) e. RR* )
100 50 3adant3
 |-  ( ( ph /\ x = +oo /\ B < x ) -> x e. RR* )
101 100 ad3antrrr
 |-  ( ( ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) /\ y e. A ) /\ y < ( B + 1 ) ) -> x e. RR* )
102 simpr
 |-  ( ( ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) /\ y e. A ) /\ y < ( B + 1 ) ) -> y < ( B + 1 ) )
103 80 ltpnfd
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> ( B + 1 ) < +oo )
104 56 adantr
 |-  ( ( x = +oo /\ -. B = -oo ) -> +oo = x )
105 104 3ad2antl2
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> +oo = x )
106 103 105 breqtrd
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> ( B + 1 ) < x )
107 106 ad2antrr
 |-  ( ( ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) /\ y e. A ) /\ y < ( B + 1 ) ) -> ( B + 1 ) < x )
108 96 99 101 102 107 xrlttrd
 |-  ( ( ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) /\ y e. A ) /\ y < ( B + 1 ) ) -> y < x )
109 108 ex
 |-  ( ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) /\ y e. A ) -> ( y < ( B + 1 ) -> y < x ) )
110 109 ex
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> ( y e. A -> ( y < ( B + 1 ) -> y < x ) ) )
111 94 110 reximdai
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> ( E. y e. A y < ( B + 1 ) -> E. y e. A y < x ) )
112 90 111 mpd
 |-  ( ( ( ph /\ x = +oo /\ B < x ) /\ -. B = -oo ) -> E. y e. A y < x )
113 66 112 pm2.61dan
 |-  ( ( ph /\ x = +oo /\ B < x ) -> E. y e. A y < x )
114 9 23 24 113 syl3anc
 |-  ( ( ( ( ph /\ x e. RR* ) /\ -. x e. RR ) /\ B < x ) -> E. y e. A y < x )
115 114 ex
 |-  ( ( ( ph /\ x e. RR* ) /\ -. x e. RR ) -> ( B < x -> E. y e. A y < x ) )
116 8 115 pm2.61dan
 |-  ( ( ph /\ x e. RR* ) -> ( B < x -> E. y e. A y < x ) )
117 116 ex
 |-  ( ph -> ( x e. RR* -> ( B < x -> E. y e. A y < x ) ) )
118 1 117 ralrimi
 |-  ( ph -> A. x e. RR* ( B < x -> E. y e. A y < x ) )
119 xrltso
 |-  < Or RR*
120 119 a1i
 |-  ( T. -> < Or RR* )
121 120 eqinf
 |-  ( T. -> ( ( B e. RR* /\ A. x e. A -. x < B /\ A. x e. RR* ( B < x -> E. y e. A y < x ) ) -> inf ( A , RR* , < ) = B ) )
122 121 mptru
 |-  ( ( B e. RR* /\ A. x e. A -. x < B /\ A. x e. RR* ( B < x -> E. y e. A y < x ) ) -> inf ( A , RR* , < ) = B )
123 4 5 118 122 syl3anc
 |-  ( ph -> inf ( A , RR* , < ) = B )