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 ffvelcdmda 
 |-  ( ( 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 ) ) )