Metamath Proof Explorer

Theorem rfcnnnub

Description: Given a real continuous function F defined on a compact topological space, there is always a positive integer that is a strict upper bound of its range. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses rfcnnnub.1 
|- F/_ t F
rfcnnnub.2 
|- F/ t ph
rfcnnnub.3 
|- K = ( topGen ` ran (,) )
rfcnnnub.4 
|- ( ph -> J e. Comp )
rfcnnnub.5 
|- T = U. J
rfcnnnub.6 
|- ( ph -> T =/= (/) )
rfcnnnub.7 
|- C = ( J Cn K )
rfcnnnub.8 
|- ( ph -> F e. C )
Assertion rfcnnnub 
|- ( ph -> E. n e. NN A. t e. T ( F ` t ) < n )

Proof

Step Hyp Ref Expression
1 rfcnnnub.1 
 |-  F/_ t F
2 rfcnnnub.2 
 |-  F/ t ph
3 rfcnnnub.3 
 |-  K = ( topGen ` ran (,) )
4 rfcnnnub.4 
 |-  ( ph -> J e. Comp )
5 rfcnnnub.5 
 |-  T = U. J
6 rfcnnnub.6 
 |-  ( ph -> T =/= (/) )
7 rfcnnnub.7 
 |-  C = ( J Cn K )
8 rfcnnnub.8 
 |-  ( ph -> F e. C )
9 nfcv 
 |-  F/_ s F
10 nfcv 
 |-  F/_ s T
11 nfcv 
 |-  F/_ t T
12 nfv 
 |-  F/ s ph
13 8 7 eleqtrdi 
 |-  ( ph -> F e. ( J Cn K ) )
14 9 1 10 11 12 2 5 3 4 13 6 evthf 
 |-  ( ph -> E. s e. T A. t e. T ( F ` t ) <_ ( F ` s ) )
15 df-rex 
 |-  ( E. s e. T A. t e. T ( F ` t ) <_ ( F ` s ) <-> E. s ( s e. T /\ A. t e. T ( F ` t ) <_ ( F ` s ) ) )
16 14 15 sylib 
 |-  ( ph -> E. s ( s e. T /\ A. t e. T ( F ` t ) <_ ( F ` s ) ) )
17 3 5 7 8 fcnre 
 |-  ( ph -> F : T --> RR )
18 17 ffvelcdmda 
 |-  ( ( ph /\ s e. T ) -> ( F ` s ) e. RR )
19 18 ex 
 |-  ( ph -> ( s e. T -> ( F ` s ) e. RR ) )
20 19 anim1d 
 |-  ( ph -> ( ( s e. T /\ A. t e. T ( F ` t ) <_ ( F ` s ) ) -> ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) ) ) )
21 20 eximdv 
 |-  ( ph -> ( E. s ( s e. T /\ A. t e. T ( F ` t ) <_ ( F ` s ) ) -> E. s ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) ) ) )
22 16 21 mpd 
 |-  ( ph -> E. s ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) ) )
23 17 ffvelcdmda 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) e. RR )
24 23 ex 
 |-  ( ph -> ( t e. T -> ( F ` t ) e. RR ) )
25 2 24 ralrimi 
 |-  ( ph -> A. t e. T ( F ` t ) e. RR )
26 19.41v 
 |-  ( E. s ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) ) /\ A. t e. T ( F ` t ) e. RR ) <-> ( E. s ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) ) /\ A. t e. T ( F ` t ) e. RR ) )
27 22 25 26 sylanbrc 
 |-  ( ph -> E. s ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) ) /\ A. t e. T ( F ` t ) e. RR ) )
28 df-3an 
 |-  ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) <-> ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) ) /\ A. t e. T ( F ` t ) e. RR ) )
29 28 exbii 
 |-  ( E. s ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) <-> E. s ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) ) /\ A. t e. T ( F ` t ) e. RR ) )
30 27 29 sylibr 
 |-  ( ph -> E. s ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) )
31 nfcv 
 |-  F/_ t s
32 1 31 nffv 
 |-  F/_ t ( F ` s )
33 32 nfel1 
 |-  F/ t ( F ` s ) e. RR
34 nfra1 
 |-  F/ t A. t e. T ( F ` t ) <_ ( F ` s )
35 nfra1 
 |-  F/ t A. t e. T ( F ` t ) e. RR
36 33 34 35 nf3an 
 |-  F/ t ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR )
37 nfv 
 |-  F/ t n e. NN
38 nfcv 
 |-  F/_ t <
39 nfcv 
 |-  F/_ t n
40 32 38 39 nfbr 
 |-  F/ t ( F ` s ) < n
41 37 40 nfan 
 |-  F/ t ( n e. NN /\ ( F ` s ) < n )
42 36 41 nfan 
 |-  F/ t ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) /\ ( n e. NN /\ ( F ` s ) < n ) )
43 simpll3 
 |-  ( ( ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) /\ ( n e. NN /\ ( F ` s ) < n ) ) /\ t e. T ) -> A. t e. T ( F ` t ) e. RR )
44 simpr 
 |-  ( ( ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) /\ ( n e. NN /\ ( F ` s ) < n ) ) /\ t e. T ) -> t e. T )
45 rsp 
 |-  ( A. t e. T ( F ` t ) e. RR -> ( t e. T -> ( F ` t ) e. RR ) )
46 43 44 45 sylc 
 |-  ( ( ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) /\ ( n e. NN /\ ( F ` s ) < n ) ) /\ t e. T ) -> ( F ` t ) e. RR )
47 simpll1 
 |-  ( ( ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) /\ ( n e. NN /\ ( F ` s ) < n ) ) /\ t e. T ) -> ( F ` s ) e. RR )
48 simplrl 
 |-  ( ( ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) /\ ( n e. NN /\ ( F ` s ) < n ) ) /\ t e. T ) -> n e. NN )
49 48 nnred 
 |-  ( ( ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) /\ ( n e. NN /\ ( F ` s ) < n ) ) /\ t e. T ) -> n e. RR )
50 simpl2 
 |-  ( ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) /\ ( n e. NN /\ ( F ` s ) < n ) ) -> A. t e. T ( F ` t ) <_ ( F ` s ) )
51 50 r19.21bi 
 |-  ( ( ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) /\ ( n e. NN /\ ( F ` s ) < n ) ) /\ t e. T ) -> ( F ` t ) <_ ( F ` s ) )
52 simplrr 
 |-  ( ( ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) /\ ( n e. NN /\ ( F ` s ) < n ) ) /\ t e. T ) -> ( F ` s ) < n )
53 46 47 49 51 52 lelttrd 
 |-  ( ( ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) /\ ( n e. NN /\ ( F ` s ) < n ) ) /\ t e. T ) -> ( F ` t ) < n )
54 53 ex 
 |-  ( ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) /\ ( n e. NN /\ ( F ` s ) < n ) ) -> ( t e. T -> ( F ` t ) < n ) )
55 42 54 ralrimi 
 |-  ( ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) /\ ( n e. NN /\ ( F ` s ) < n ) ) -> A. t e. T ( F ` t ) < n )
56 arch 
 |-  ( ( F ` s ) e. RR -> E. n e. NN ( F ` s ) < n )
57 56 3ad2ant1 
 |-  ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) -> E. n e. NN ( F ` s ) < n )
58 55 57 reximddv 
 |-  ( ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) -> E. n e. NN A. t e. T ( F ` t ) < n )
59 58 eximi 
 |-  ( E. s ( ( F ` s ) e. RR /\ A. t e. T ( F ` t ) <_ ( F ` s ) /\ A. t e. T ( F ` t ) e. RR ) -> E. s E. n e. NN A. t e. T ( F ` t ) < n )
60 30 59 syl 
 |-  ( ph -> E. s E. n e. NN A. t e. T ( F ` t ) < n )
61 19.9v 
 |-  ( E. s E. n e. NN A. t e. T ( F ` t ) < n <-> E. n e. NN A. t e. T ( F ` t ) < n )
62 60 61 sylib 
 |-  ( ph -> E. n e. NN A. t e. T ( F ` t ) < n )