Metamath Proof Explorer

Theorem cncmpmax

Description: When the hypothesis for the extreme value theorem hold, then the sup of the range of the function belongs to the range, it is real and it an upper bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses cncmpmax.1 
|- T = U. J
cncmpmax.2 
|- K = ( topGen ` ran (,) )
cncmpmax.3 
|- ( ph -> J e. Comp )
cncmpmax.4 
|- ( ph -> F e. ( J Cn K ) )
cncmpmax.5 
|- ( ph -> T =/= (/) )
Assertion cncmpmax 
|- ( ph -> ( sup ( ran F , RR , < ) e. ran F /\ sup ( ran F , RR , < ) e. RR /\ A. t e. T ( F ` t ) <_ sup ( ran F , RR , < ) ) )

Proof

Step Hyp Ref Expression
1 cncmpmax.1 
 |-  T = U. J
2 cncmpmax.2 
 |-  K = ( topGen ` ran (,) )
3 cncmpmax.3 
 |-  ( ph -> J e. Comp )
4 cncmpmax.4 
 |-  ( ph -> F e. ( J Cn K ) )
5 cncmpmax.5 
 |-  ( ph -> T =/= (/) )
6 1 2 3 4 5 evth 
 |-  ( ph -> E. x e. T A. t e. T ( F ` t ) <_ ( F ` x ) )
7 eqid 
 |-  ( J Cn K ) = ( J Cn K )
8 2 1 7 4 fcnre 
 |-  ( ph -> F : T --> RR )
9 8 frnd 
 |-  ( ph -> ran F C_ RR )
10 9 adantr 
 |-  ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> ran F C_ RR )
11 8 ffund 
 |-  ( ph -> Fun F )
12 11 adantr 
 |-  ( ( ph /\ x e. T ) -> Fun F )
13 simpr 
 |-  ( ( ph /\ x e. T ) -> x e. T )
14 8 adantr 
 |-  ( ( ph /\ x e. T ) -> F : T --> RR )
15 14 fdmd 
 |-  ( ( ph /\ x e. T ) -> dom F = T )
16 13 15 eleqtrrd 
 |-  ( ( ph /\ x e. T ) -> x e. dom F )
17 fvelrn 
 |-  ( ( Fun F /\ x e. dom F ) -> ( F ` x ) e. ran F )
18 12 16 17 syl2anc 
 |-  ( ( ph /\ x e. T ) -> ( F ` x ) e. ran F )
19 18 adantrr 
 |-  ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> ( F ` x ) e. ran F )
20 ffn 
 |-  ( F : T --> RR -> F Fn T )
21 fvelrnb 
 |-  ( F Fn T -> ( y e. ran F <-> E. s e. T ( F ` s ) = y ) )
22 8 20 21 3syl 
 |-  ( ph -> ( y e. ran F <-> E. s e. T ( F ` s ) = y ) )
23 22 biimpa 
 |-  ( ( ph /\ y e. ran F ) -> E. s e. T ( F ` s ) = y )
24 df-rex 
 |-  ( E. s e. T ( F ` s ) = y <-> E. s ( s e. T /\ ( F ` s ) = y ) )
25 23 24 sylib 
 |-  ( ( ph /\ y e. ran F ) -> E. s ( s e. T /\ ( F ` s ) = y ) )
26 25 adantlr 
 |-  ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) -> E. s ( s e. T /\ ( F ` s ) = y ) )
27 simprr 
 |-  ( ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) /\ ( s e. T /\ ( F ` s ) = y ) ) -> ( F ` s ) = y )
28 simpllr 
 |-  ( ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) /\ ( s e. T /\ ( F ` s ) = y ) ) -> A. t e. T ( F ` t ) <_ ( F ` x ) )
29 simprl 
 |-  ( ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) /\ ( s e. T /\ ( F ` s ) = y ) ) -> s e. T )
30 fveq2 
 |-  ( t = s -> ( F ` t ) = ( F ` s ) )
31 30 breq1d 
 |-  ( t = s -> ( ( F ` t ) <_ ( F ` x ) <-> ( F ` s ) <_ ( F ` x ) ) )
32 31 rspccva 
 |-  ( ( A. t e. T ( F ` t ) <_ ( F ` x ) /\ s e. T ) -> ( F ` s ) <_ ( F ` x ) )
33 28 29 32 syl2anc 
 |-  ( ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) /\ ( s e. T /\ ( F ` s ) = y ) ) -> ( F ` s ) <_ ( F ` x ) )
34 27 33 eqbrtrrd 
 |-  ( ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) /\ ( s e. T /\ ( F ` s ) = y ) ) -> y <_ ( F ` x ) )
35 26 34 exlimddv 
 |-  ( ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) /\ y e. ran F ) -> y <_ ( F ` x ) )
36 35 ralrimiva 
 |-  ( ( ph /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) -> A. y e. ran F y <_ ( F ` x ) )
37 36 adantrl 
 |-  ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> A. y e. ran F y <_ ( F ` x ) )
38 ubelsupr 
 |-  ( ( ran F C_ RR /\ ( F ` x ) e. ran F /\ A. y e. ran F y <_ ( F ` x ) ) -> ( F ` x ) = sup ( ran F , RR , < ) )
39 10 19 37 38 syl3anc 
 |-  ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> ( F ` x ) = sup ( ran F , RR , < ) )
40 39 eqcomd 
 |-  ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> sup ( ran F , RR , < ) = ( F ` x ) )
41 40 19 eqeltrd 
 |-  ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> sup ( ran F , RR , < ) e. ran F )
42 10 41 sseldd 
 |-  ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> sup ( ran F , RR , < ) e. RR )
43 simplrr 
 |-  ( ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) /\ s e. T ) -> A. t e. T ( F ` t ) <_ ( F ` x ) )
44 43 32 sylancom 
 |-  ( ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) /\ s e. T ) -> ( F ` s ) <_ ( F ` x ) )
45 40 adantr 
 |-  ( ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) /\ s e. T ) -> sup ( ran F , RR , < ) = ( F ` x ) )
46 44 45 breqtrrd 
 |-  ( ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) /\ s e. T ) -> ( F ` s ) <_ sup ( ran F , RR , < ) )
47 46 ralrimiva 
 |-  ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> A. s e. T ( F ` s ) <_ sup ( ran F , RR , < ) )
48 30 breq1d 
 |-  ( t = s -> ( ( F ` t ) <_ sup ( ran F , RR , < ) <-> ( F ` s ) <_ sup ( ran F , RR , < ) ) )
49 48 cbvralvw 
 |-  ( A. t e. T ( F ` t ) <_ sup ( ran F , RR , < ) <-> A. s e. T ( F ` s ) <_ sup ( ran F , RR , < ) )
50 47 49 sylibr 
 |-  ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> A. t e. T ( F ` t ) <_ sup ( ran F , RR , < ) )
51 41 42 50 3jca 
 |-  ( ( ph /\ ( x e. T /\ A. t e. T ( F ` t ) <_ ( F ` x ) ) ) -> ( sup ( ran F , RR , < ) e. ran F /\ sup ( ran F , RR , < ) e. RR /\ A. t e. T ( F ` t ) <_ sup ( ran F , RR , < ) ) )
52 6 51 rexlimddv 
 |-  ( ph -> ( sup ( ran F , RR , < ) e. ran F /\ sup ( ran F , RR , < ) e. RR /\ A. t e. T ( F ` t ) <_ sup ( ran F , RR , < ) ) )