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
|- F/_ t F
stoweidlem29.2
|- F/ t ph
stoweidlem29.3
|- T = U. J
stoweidlem29.4
|- K = ( topGen ` ran (,) )
stoweidlem29.5
|- ( ph -> J e. Comp )
stoweidlem29.6
|- ( ph -> F e. ( J Cn K ) )
stoweidlem29.7
|- ( ph -> T =/= (/) )
Assertion stoweidlem29
|- ( ph -> ( inf ( ran F , RR , < ) e. ran F /\ inf ( ran F , RR , < ) e. RR /\ A. t e. T inf ( ran F , RR , < ) <_ ( F ` t ) ) )

Proof

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