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 , < ) ) )