Metamath Proof Explorer

Theorem evth

Description: The Extreme Value Theorem. A continuous function from a nonempty compact topological space to the reals attains its maximum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Hypotheses bndth.1 
|- X = U. J
bndth.2 
|- K = ( topGen ` ran (,) )
bndth.3 
|- ( ph -> J e. Comp )
bndth.4 
|- ( ph -> F e. ( J Cn K ) )
evth.5 
|- ( ph -> X =/= (/) )
Assertion evth 
|- ( ph -> E. x e. X A. y e. X ( F ` y ) <_ ( F ` x ) )

Proof

Step Hyp Ref Expression
1 bndth.1 
 |-  X = U. J
2 bndth.2 
 |-  K = ( topGen ` ran (,) )
3 bndth.3 
 |-  ( ph -> J e. Comp )
4 bndth.4 
 |-  ( ph -> F e. ( J Cn K ) )
5 evth.5 
 |-  ( ph -> X =/= (/) )
6 3 adantr 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> J e. Comp )
7 cmptop 
 |-  ( J e. Comp -> J e. Top )
8 6 7 syl 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> J e. Top )
9 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
10 8 9 sylib 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> J e. ( TopOn ` X ) )
11 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
12 11 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
13 12 a1i 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
14 1cnd 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> 1 e. CC )
15 10 13 14 cnmptc 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( z e. X |-> 1 ) e. ( J Cn ( TopOpen ` CCfld ) ) )
16 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
17 2 unieqi 
 |-  U. K = U. ( topGen ` ran (,) )
18 16 17 eqtr4i 
 |-  RR = U. K
19 1 18 cnf 
 |-  ( F e. ( J Cn K ) -> F : X --> RR )
20 4 19 syl 
 |-  ( ph -> F : X --> RR )
21 20 frnd 
 |-  ( ph -> ran F C_ RR )
22 20 fdmd 
 |-  ( ph -> dom F = X )
23 22 5 eqnetrd 
 |-  ( ph -> dom F =/= (/) )
24 dm0rn0 
 |-  ( dom F = (/) <-> ran F = (/) )
25 24 necon3bii 
 |-  ( dom F =/= (/) <-> ran F =/= (/) )
26 23 25 sylib 
 |-  ( ph -> ran F =/= (/) )
27 1 2 3 4 bndth 
 |-  ( ph -> E. x e. RR A. y e. X ( F ` y ) <_ x )
28 20 ffnd 
 |-  ( ph -> F Fn X )
29 breq1 
 |-  ( z = ( F ` y ) -> ( z <_ x <-> ( F ` y ) <_ x ) )
30 29 ralrn 
 |-  ( F Fn X -> ( A. z e. ran F z <_ x <-> A. y e. X ( F ` y ) <_ x ) )
31 28 30 syl 
 |-  ( ph -> ( A. z e. ran F z <_ x <-> A. y e. X ( F ` y ) <_ x ) )
32 31 rexbidv 
 |-  ( ph -> ( E. x e. RR A. z e. ran F z <_ x <-> E. x e. RR A. y e. X ( F ` y ) <_ x ) )
33 27 32 mpbird 
 |-  ( ph -> E. x e. RR A. z e. ran F z <_ x )
34 21 26 33 3jca 
 |-  ( ph -> ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. z e. ran F z <_ x ) )
35 suprcl 
 |-  ( ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. z e. ran F z <_ x ) -> sup ( ran F , RR , < ) e. RR )
36 34 35 syl 
 |-  ( ph -> sup ( ran F , RR , < ) e. RR )
37 36 recnd 
 |-  ( ph -> sup ( ran F , RR , < ) e. CC )
38 37 adantr 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> sup ( ran F , RR , < ) e. CC )
39 10 13 38 cnmptc 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( z e. X |-> sup ( ran F , RR , < ) ) e. ( J Cn ( TopOpen ` CCfld ) ) )
40 20 feqmptd 
 |-  ( ph -> F = ( z e. X |-> ( F ` z ) ) )
41 11 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
42 cnrest2r 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) C_ ( J Cn ( TopOpen ` CCfld ) ) )
43 41 42 ax-mp 
 |-  ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) C_ ( J Cn ( TopOpen ` CCfld ) )
44 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
45 2 44 eqtri 
 |-  K = ( ( TopOpen ` CCfld ) |`t RR )
46 45 oveq2i 
 |-  ( J Cn K ) = ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) )
47 4 46 eleqtrdi 
 |-  ( ph -> F e. ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
48 43 47 sselid 
 |-  ( ph -> F e. ( J Cn ( TopOpen ` CCfld ) ) )
49 40 48 eqeltrrd 
 |-  ( ph -> ( z e. X |-> ( F ` z ) ) e. ( J Cn ( TopOpen ` CCfld ) ) )
50 49 adantr 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( z e. X |-> ( F ` z ) ) e. ( J Cn ( TopOpen ` CCfld ) ) )
51 11 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
52 51 a1i 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
53 10 39 50 52 cnmpt12f 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( z e. X |-> ( sup ( ran F , RR , < ) - ( F ` z ) ) ) e. ( J Cn ( TopOpen ` CCfld ) ) )
54 36 ad2antrr 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ z e. X ) -> sup ( ran F , RR , < ) e. RR )
55 ffvelcdm 
 |-  ( ( F : X --> ( RR \ { sup ( ran F , RR , < ) } ) /\ z e. X ) -> ( F ` z ) e. ( RR \ { sup ( ran F , RR , < ) } ) )
56 55 adantll 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ z e. X ) -> ( F ` z ) e. ( RR \ { sup ( ran F , RR , < ) } ) )
57 eldifsn 
 |-  ( ( F ` z ) e. ( RR \ { sup ( ran F , RR , < ) } ) <-> ( ( F ` z ) e. RR /\ ( F ` z ) =/= sup ( ran F , RR , < ) ) )
58 56 57 sylib 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ z e. X ) -> ( ( F ` z ) e. RR /\ ( F ` z ) =/= sup ( ran F , RR , < ) ) )
59 58 simpld 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ z e. X ) -> ( F ` z ) e. RR )
60 54 59 resubcld 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ z e. X ) -> ( sup ( ran F , RR , < ) - ( F ` z ) ) e. RR )
61 60 recnd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ z e. X ) -> ( sup ( ran F , RR , < ) - ( F ` z ) ) e. CC )
62 54 recnd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ z e. X ) -> sup ( ran F , RR , < ) e. CC )
63 59 recnd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ z e. X ) -> ( F ` z ) e. CC )
64 58 simprd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ z e. X ) -> ( F ` z ) =/= sup ( ran F , RR , < ) )
65 64 necomd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ z e. X ) -> sup ( ran F , RR , < ) =/= ( F ` z ) )
66 62 63 65 subne0d 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ z e. X ) -> ( sup ( ran F , RR , < ) - ( F ` z ) ) =/= 0 )
67 eldifsn 
 |-  ( ( sup ( ran F , RR , < ) - ( F ` z ) ) e. ( CC \ { 0 } ) <-> ( ( sup ( ran F , RR , < ) - ( F ` z ) ) e. CC /\ ( sup ( ran F , RR , < ) - ( F ` z ) ) =/= 0 ) )
68 61 66 67 sylanbrc 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ z e. X ) -> ( sup ( ran F , RR , < ) - ( F ` z ) ) e. ( CC \ { 0 } ) )
69 68 fmpttd 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( z e. X |-> ( sup ( ran F , RR , < ) - ( F ` z ) ) ) : X --> ( CC \ { 0 } ) )
70 69 frnd 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ran ( z e. X |-> ( sup ( ran F , RR , < ) - ( F ` z ) ) ) C_ ( CC \ { 0 } ) )
71 difssd 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( CC \ { 0 } ) C_ CC )
72 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( z e. X |-> ( sup ( ran F , RR , < ) - ( F ` z ) ) ) C_ ( CC \ { 0 } ) /\ ( CC \ { 0 } ) C_ CC ) -> ( ( z e. X |-> ( sup ( ran F , RR , < ) - ( F ` z ) ) ) e. ( J Cn ( TopOpen ` CCfld ) ) <-> ( z e. X |-> ( sup ( ran F , RR , < ) - ( F ` z ) ) ) e. ( J Cn ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) ) )
73 13 70 71 72 syl3anc 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( ( z e. X |-> ( sup ( ran F , RR , < ) - ( F ` z ) ) ) e. ( J Cn ( TopOpen ` CCfld ) ) <-> ( z e. X |-> ( sup ( ran F , RR , < ) - ( F ` z ) ) ) e. ( J Cn ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) ) )
74 53 73 mpbid 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( z e. X |-> ( sup ( ran F , RR , < ) - ( F ` z ) ) ) e. ( J Cn ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) )
75 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) )
76 11 75 divcn 
 |-  / e. ( ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) Cn ( TopOpen ` CCfld ) )
77 76 a1i 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> / e. ( ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) Cn ( TopOpen ` CCfld ) ) )
78 10 15 74 77 cnmpt12f 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) e. ( J Cn ( TopOpen ` CCfld ) ) )
79 60 66 rereccld 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ z e. X ) -> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) e. RR )
80 79 fmpttd 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) : X --> RR )
81 80 frnd 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ran ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) C_ RR )
82 ax-resscn 
 |-  RR C_ CC
83 82 a1i 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> RR C_ CC )
84 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) C_ RR /\ RR C_ CC ) -> ( ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) e. ( J Cn ( TopOpen ` CCfld ) ) <-> ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) e. ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
85 13 81 83 84 syl3anc 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) e. ( J Cn ( TopOpen ` CCfld ) ) <-> ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) e. ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
86 78 85 mpbid 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) e. ( J Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
87 86 46 eleqtrrdi 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) e. ( J Cn K ) )
88 1 2 6 87 bndth 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> E. x e. RR A. y e. X ( ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) ` y ) <_ x )
89 36 ad2antrr 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> sup ( ran F , RR , < ) e. RR )
90 simpr 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> x e. RR )
91 1re 
 |-  1 e. RR
92 ifcl 
 |-  ( ( x e. RR /\ 1 e. RR ) -> if ( 1 <_ x , x , 1 ) e. RR )
93 90 91 92 sylancl 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> if ( 1 <_ x , x , 1 ) e. RR )
94 0red 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> 0 e. RR )
95 91 a1i 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> 1 e. RR )
96 0lt1 
 |-  0 < 1
97 96 a1i 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> 0 < 1 )
98 max1 
 |-  ( ( 1 e. RR /\ x e. RR ) -> 1 <_ if ( 1 <_ x , x , 1 ) )
99 91 90 98 sylancr 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> 1 <_ if ( 1 <_ x , x , 1 ) )
100 94 95 93 97 99 ltletrd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> 0 < if ( 1 <_ x , x , 1 ) )
101 100 gt0ne0d 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> if ( 1 <_ x , x , 1 ) =/= 0 )
102 93 101 rereccld 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> ( 1 / if ( 1 <_ x , x , 1 ) ) e. RR )
103 93 100 recgt0d 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> 0 < ( 1 / if ( 1 <_ x , x , 1 ) ) )
104 102 103 elrpd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> ( 1 / if ( 1 <_ x , x , 1 ) ) e. RR+ )
105 89 104 ltsubrpd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) < sup ( ran F , RR , < ) )
106 89 102 resubcld 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) e. RR )
107 106 89 ltnled 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> ( ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) < sup ( ran F , RR , < ) <-> -. sup ( ran F , RR , < ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
108 105 107 mpbid 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> -. sup ( ran F , RR , < ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) )
109 simprl 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> x e. RR )
110 max2 
 |-  ( ( 1 e. RR /\ x e. RR ) -> x <_ if ( 1 <_ x , x , 1 ) )
111 91 109 110 sylancr 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> x <_ if ( 1 <_ x , x , 1 ) )
112 36 ad2antrr 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> sup ( ran F , RR , < ) e. RR )
113 ffvelcdm 
 |-  ( ( F : X --> ( RR \ { sup ( ran F , RR , < ) } ) /\ y e. X ) -> ( F ` y ) e. ( RR \ { sup ( ran F , RR , < ) } ) )
114 113 ad2ant2l 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( F ` y ) e. ( RR \ { sup ( ran F , RR , < ) } ) )
115 eldifsn 
 |-  ( ( F ` y ) e. ( RR \ { sup ( ran F , RR , < ) } ) <-> ( ( F ` y ) e. RR /\ ( F ` y ) =/= sup ( ran F , RR , < ) ) )
116 114 115 sylib 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( ( F ` y ) e. RR /\ ( F ` y ) =/= sup ( ran F , RR , < ) ) )
117 116 simpld 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( F ` y ) e. RR )
118 112 117 resubcld 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( sup ( ran F , RR , < ) - ( F ` y ) ) e. RR )
119 fnfvelrn 
 |-  ( ( F Fn X /\ y e. X ) -> ( F ` y ) e. ran F )
120 28 119 sylan 
 |-  ( ( ph /\ y e. X ) -> ( F ` y ) e. ran F )
121 suprub 
 |-  ( ( ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. z e. ran F z <_ x ) /\ ( F ` y ) e. ran F ) -> ( F ` y ) <_ sup ( ran F , RR , < ) )
122 34 120 121 syl2an2r 
 |-  ( ( ph /\ y e. X ) -> ( F ` y ) <_ sup ( ran F , RR , < ) )
123 122 ad2ant2rl 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( F ` y ) <_ sup ( ran F , RR , < ) )
124 116 simprd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( F ` y ) =/= sup ( ran F , RR , < ) )
125 124 necomd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> sup ( ran F , RR , < ) =/= ( F ` y ) )
126 117 112 123 125 leneltd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( F ` y ) < sup ( ran F , RR , < ) )
127 117 112 posdifd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( ( F ` y ) < sup ( ran F , RR , < ) <-> 0 < ( sup ( ran F , RR , < ) - ( F ` y ) ) ) )
128 126 127 mpbid 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> 0 < ( sup ( ran F , RR , < ) - ( F ` y ) ) )
129 128 gt0ne0d 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( sup ( ran F , RR , < ) - ( F ` y ) ) =/= 0 )
130 118 129 rereccld 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) e. RR )
131 109 91 92 sylancl 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> if ( 1 <_ x , x , 1 ) e. RR )
132 letr 
 |-  ( ( ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) e. RR /\ x e. RR /\ if ( 1 <_ x , x , 1 ) e. RR ) -> ( ( ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) <_ x /\ x <_ if ( 1 <_ x , x , 1 ) ) -> ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) <_ if ( 1 <_ x , x , 1 ) ) )
133 130 109 131 132 syl3anc 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( ( ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) <_ x /\ x <_ if ( 1 <_ x , x , 1 ) ) -> ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) <_ if ( 1 <_ x , x , 1 ) ) )
134 111 133 mpan2d 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) <_ x -> ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) <_ if ( 1 <_ x , x , 1 ) ) )
135 fveq2 
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
136 135 oveq2d 
 |-  ( z = y -> ( sup ( ran F , RR , < ) - ( F ` z ) ) = ( sup ( ran F , RR , < ) - ( F ` y ) ) )
137 136 oveq2d 
 |-  ( z = y -> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) = ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) )
138 eqid 
 |-  ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) = ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) )
139 ovex 
 |-  ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) e. _V
140 137 138 139 fvmpt 
 |-  ( y e. X -> ( ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) ` y ) = ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) )
141 140 breq1d 
 |-  ( y e. X -> ( ( ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) ` y ) <_ x <-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) <_ x ) )
142 141 ad2antll 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( ( ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) ` y ) <_ x <-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) <_ x ) )
143 102 adantrr 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( 1 / if ( 1 <_ x , x , 1 ) ) e. RR )
144 100 adantrr 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> 0 < if ( 1 <_ x , x , 1 ) )
145 131 144 recgt0d 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> 0 < ( 1 / if ( 1 <_ x , x , 1 ) ) )
146 lerec 
 |-  ( ( ( ( 1 / if ( 1 <_ x , x , 1 ) ) e. RR /\ 0 < ( 1 / if ( 1 <_ x , x , 1 ) ) ) /\ ( ( sup ( ran F , RR , < ) - ( F ` y ) ) e. RR /\ 0 < ( sup ( ran F , RR , < ) - ( F ` y ) ) ) ) -> ( ( 1 / if ( 1 <_ x , x , 1 ) ) <_ ( sup ( ran F , RR , < ) - ( F ` y ) ) <-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) <_ ( 1 / ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
147 143 145 118 128 146 syl22anc 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( ( 1 / if ( 1 <_ x , x , 1 ) ) <_ ( sup ( ran F , RR , < ) - ( F ` y ) ) <-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) <_ ( 1 / ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
148 lesub 
 |-  ( ( ( 1 / if ( 1 <_ x , x , 1 ) ) e. RR /\ sup ( ran F , RR , < ) e. RR /\ ( F ` y ) e. RR ) -> ( ( 1 / if ( 1 <_ x , x , 1 ) ) <_ ( sup ( ran F , RR , < ) - ( F ` y ) ) <-> ( F ` y ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
149 143 112 117 148 syl3anc 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( ( 1 / if ( 1 <_ x , x , 1 ) ) <_ ( sup ( ran F , RR , < ) - ( F ` y ) ) <-> ( F ` y ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
150 131 recnd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> if ( 1 <_ x , x , 1 ) e. CC )
151 101 adantrr 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> if ( 1 <_ x , x , 1 ) =/= 0 )
152 150 151 recrecd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( 1 / ( 1 / if ( 1 <_ x , x , 1 ) ) ) = if ( 1 <_ x , x , 1 ) )
153 152 breq2d 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) <_ ( 1 / ( 1 / if ( 1 <_ x , x , 1 ) ) ) <-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) <_ if ( 1 <_ x , x , 1 ) ) )
154 147 149 153 3bitr3d 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( ( F ` y ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) <-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` y ) ) ) <_ if ( 1 <_ x , x , 1 ) ) )
155 134 142 154 3imtr4d 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ ( x e. RR /\ y e. X ) ) -> ( ( ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) ` y ) <_ x -> ( F ` y ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
156 155 anassrs 
 |-  ( ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) /\ y e. X ) -> ( ( ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) ` y ) <_ x -> ( F ` y ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
157 156 ralimdva 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> ( A. y e. X ( ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) ` y ) <_ x -> A. y e. X ( F ` y ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
158 34 ad2antrr 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. z e. ran F z <_ x ) )
159 suprleub 
 |-  ( ( ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. z e. ran F z <_ x ) /\ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) e. RR ) -> ( sup ( ran F , RR , < ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) <-> A. z e. ran F z <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
160 158 106 159 syl2anc 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> ( sup ( ran F , RR , < ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) <-> A. z e. ran F z <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
161 28 ad2antrr 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> F Fn X )
162 breq1 
 |-  ( z = ( F ` y ) -> ( z <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) <-> ( F ` y ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
163 162 ralrn 
 |-  ( F Fn X -> ( A. z e. ran F z <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) <-> A. y e. X ( F ` y ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
164 161 163 syl 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> ( A. z e. ran F z <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) <-> A. y e. X ( F ` y ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
165 160 164 bitrd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> ( sup ( ran F , RR , < ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) <-> A. y e. X ( F ` y ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
166 157 165 sylibrd 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> ( A. y e. X ( ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) ` y ) <_ x -> sup ( ran F , RR , < ) <_ ( sup ( ran F , RR , < ) - ( 1 / if ( 1 <_ x , x , 1 ) ) ) ) )
167 108 166 mtod 
 |-  ( ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) /\ x e. RR ) -> -. A. y e. X ( ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) ` y ) <_ x )
168 167 nrexdv 
 |-  ( ( ph /\ F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) -> -. E. x e. RR A. y e. X ( ( z e. X |-> ( 1 / ( sup ( ran F , RR , < ) - ( F ` z ) ) ) ) ` y ) <_ x )
169 88 168 pm2.65da 
 |-  ( ph -> -. F : X --> ( RR \ { sup ( ran F , RR , < ) } ) )
170 122 ralrimiva 
 |-  ( ph -> A. y e. X ( F ` y ) <_ sup ( ran F , RR , < ) )
171 breq2 
 |-  ( ( F ` x ) = sup ( ran F , RR , < ) -> ( ( F ` y ) <_ ( F ` x ) <-> ( F ` y ) <_ sup ( ran F , RR , < ) ) )
172 171 ralbidv 
 |-  ( ( F ` x ) = sup ( ran F , RR , < ) -> ( A. y e. X ( F ` y ) <_ ( F ` x ) <-> A. y e. X ( F ` y ) <_ sup ( ran F , RR , < ) ) )
173 170 172 syl5ibrcom 
 |-  ( ph -> ( ( F ` x ) = sup ( ran F , RR , < ) -> A. y e. X ( F ` y ) <_ ( F ` x ) ) )
174 173 necon3bd 
 |-  ( ph -> ( -. A. y e. X ( F ` y ) <_ ( F ` x ) -> ( F ` x ) =/= sup ( ran F , RR , < ) ) )
175 174 adantr 
 |-  ( ( ph /\ x e. X ) -> ( -. A. y e. X ( F ` y ) <_ ( F ` x ) -> ( F ` x ) =/= sup ( ran F , RR , < ) ) )
176 20 ffvelcdmda 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. RR )
177 eldifsn 
 |-  ( ( F ` x ) e. ( RR \ { sup ( ran F , RR , < ) } ) <-> ( ( F ` x ) e. RR /\ ( F ` x ) =/= sup ( ran F , RR , < ) ) )
178 177 baib 
 |-  ( ( F ` x ) e. RR -> ( ( F ` x ) e. ( RR \ { sup ( ran F , RR , < ) } ) <-> ( F ` x ) =/= sup ( ran F , RR , < ) ) )
179 176 178 syl 
 |-  ( ( ph /\ x e. X ) -> ( ( F ` x ) e. ( RR \ { sup ( ran F , RR , < ) } ) <-> ( F ` x ) =/= sup ( ran F , RR , < ) ) )
180 175 179 sylibrd 
 |-  ( ( ph /\ x e. X ) -> ( -. A. y e. X ( F ` y ) <_ ( F ` x ) -> ( F ` x ) e. ( RR \ { sup ( ran F , RR , < ) } ) ) )
181 180 ralimdva 
 |-  ( ph -> ( A. x e. X -. A. y e. X ( F ` y ) <_ ( F ` x ) -> A. x e. X ( F ` x ) e. ( RR \ { sup ( ran F , RR , < ) } ) ) )
182 ffnfv 
 |-  ( F : X --> ( RR \ { sup ( ran F , RR , < ) } ) <-> ( F Fn X /\ A. x e. X ( F ` x ) e. ( RR \ { sup ( ran F , RR , < ) } ) ) )
183 182 baib 
 |-  ( F Fn X -> ( F : X --> ( RR \ { sup ( ran F , RR , < ) } ) <-> A. x e. X ( F ` x ) e. ( RR \ { sup ( ran F , RR , < ) } ) ) )
184 28 183 syl 
 |-  ( ph -> ( F : X --> ( RR \ { sup ( ran F , RR , < ) } ) <-> A. x e. X ( F ` x ) e. ( RR \ { sup ( ran F , RR , < ) } ) ) )
185 181 184 sylibrd 
 |-  ( ph -> ( A. x e. X -. A. y e. X ( F ` y ) <_ ( F ` x ) -> F : X --> ( RR \ { sup ( ran F , RR , < ) } ) ) )
186 169 185 mtod 
 |-  ( ph -> -. A. x e. X -. A. y e. X ( F ` y ) <_ ( F ` x ) )
187 dfrex2 
 |-  ( E. x e. X A. y e. X ( F ` y ) <_ ( F ` x ) <-> -. A. x e. X -. A. y e. X ( F ` y ) <_ ( F ` x ) )
188 186 187 sylibr 
 |-  ( ph -> E. x e. X A. y e. X ( F ` y ) <_ ( F ` x ) )