Metamath Proof Explorer


Theorem stoweidlem29

Description: When the hypothesis for the extreme value theorem hold, then the inf of the range of the function belongs to the range, it is real and it a lower bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypotheses stoweidlem29.1 _ t F
stoweidlem29.2 t φ
stoweidlem29.3 T = J
stoweidlem29.4 K = topGen ran .
stoweidlem29.5 φ J Comp
stoweidlem29.6 φ F J Cn K
stoweidlem29.7 φ T
Assertion stoweidlem29 φ sup ran F < ran F sup ran F < t T sup ran F < F t

Proof

Step Hyp Ref Expression
1 stoweidlem29.1 _ t F
2 stoweidlem29.2 t φ
3 stoweidlem29.3 T = J
4 stoweidlem29.4 K = topGen ran .
5 stoweidlem29.5 φ J Comp
6 stoweidlem29.6 φ F J Cn K
7 stoweidlem29.7 φ T
8 eqid J Cn K = J Cn K
9 4 3 8 6 fcnre φ F : T
10 df-f F : T F Fn T ran F
11 9 10 sylib φ F Fn T ran F
12 11 simprd φ ran F
13 11 simpld φ F Fn T
14 fnfun F Fn T Fun F
15 13 14 syl φ Fun F
16 15 adantr φ s T Fun F
17 9 fdmd φ dom F = T
18 17 eqcomd φ T = dom F
19 18 eleq2d φ s T s dom F
20 19 biimpa φ s T s dom F
21 fvelrn Fun F s dom F F s ran F
22 16 20 21 syl2anc φ s T F s ran F
23 nfcv _ t s
24 1 23 nffv _ t F s
25 24 nfeq2 t x = F s
26 breq1 x = F s x F t F s F t
27 25 26 ralbid x = F s t T x F t t T F s F t
28 27 rspcev F s ran F t T F s F t x ran F t T x F t
29 22 28 sylan φ s T t T F s F t x ran F t T x F t
30 nfcv _ s F
31 nfcv _ s T
32 nfcv _ t T
33 30 1 31 32 3 4 5 6 7 evth2f φ s T t T F s F t
34 29 33 r19.29a φ x ran F t T x F t
35 nfv y φ t T x F t
36 simpr φ t T x F t y ran F y ran F
37 13 ad2antrr φ t T x F t y ran F F Fn T
38 nfcv _ t y
39 32 38 1 fvelrnbf F Fn T y ran F t T F t = y
40 37 39 syl φ t T x F t y ran F y ran F t T F t = y
41 36 40 mpbid φ t T x F t y ran F t T F t = y
42 nfra1 t t T x F t
43 2 42 nfan t φ t T x F t
44 1 nfrn _ t ran F
45 44 nfcri t y ran F
46 43 45 nfan t φ t T x F t y ran F
47 nfv t x y
48 rspa t T x F t t T x F t
49 breq2 F t = y x F t x y
50 48 49 syl5ibcom t T x F t t T F t = y x y
51 50 ex t T x F t t T F t = y x y
52 51 ad2antlr φ t T x F t y ran F t T F t = y x y
53 46 47 52 rexlimd φ t T x F t y ran F t T F t = y x y
54 41 53 mpd φ t T x F t y ran F x y
55 54 ex φ t T x F t y ran F x y
56 35 55 ralrimi φ t T x F t y ran F x y
57 56 ex φ t T x F t y ran F x y
58 57 reximdv φ x ran F t T x F t x ran F y ran F x y
59 34 58 mpd φ x ran F y ran F x y
60 lbinfcl ran F x ran F y ran F x y sup ran F < ran F
61 12 59 60 syl2anc φ sup ran F < ran F
62 12 61 sseldd φ sup ran F <
63 12 adantr φ t T ran F
64 59 adantr φ t T x ran F y ran F x y
65 dffn3 F Fn T F : T ran F
66 13 65 sylib φ F : T ran F
67 66 ffvelrnda φ t T F t ran F
68 lbinfle ran F x ran F y ran F x y F t ran F sup ran F < F t
69 63 64 67 68 syl3anc φ t T sup ran F < F t
70 69 ex φ t T sup ran F < F t
71 2 70 ralrimi φ t T sup ran F < F t
72 61 62 71 3jca φ sup ran F < ran F sup ran F < t T sup ran F < F t