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 )