Metamath Proof Explorer

Theorem poimir

Description: Poincare-Miranda theorem. Theorem on Kulpa p. 547. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 
|- ( ph -> N e. NN )
poimir.i 
|- I = ( ( 0 [,] 1 ) ^m ( 1 ... N ) )
poimir.r 
|- R = ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) )
poimir.1 
|- ( ph -> F e. ( ( R |`t I ) Cn R ) )
poimir.2 
|- ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 0 ) ) -> ( ( F ` z ) ` n ) <_ 0 )
poimir.3 
|- ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 1 ) ) -> 0 <_ ( ( F ` z ) ` n ) )
Assertion poimir 
|- ( ph -> E. c e. I ( F ` c ) = ( ( 1 ... N ) X. { 0 } ) )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimir.i 
 |-  I = ( ( 0 [,] 1 ) ^m ( 1 ... N ) )
3 poimir.r 
 |-  R = ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) )
4 poimir.1 
 |-  ( ph -> F e. ( ( R |`t I ) Cn R ) )
5 poimir.2 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 0 ) ) -> ( ( F ` z ) ` n ) <_ 0 )
6 poimir.3 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 1 ) ) -> 0 <_ ( ( F ` z ) ` n ) )
7 1 2 3 4 5 6 poimirlem32 
 |-  ( ph -> E. c e. I A. n e. ( 1 ... N ) A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
8 ovex 
 |-  ( 1 ... N ) e. _V
9 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
10 3 pttoponconst 
 |-  ( ( ( 1 ... N ) e. _V /\ ( topGen ` ran (,) ) e. ( TopOn ` RR ) ) -> R e. ( TopOn ` ( RR ^m ( 1 ... N ) ) ) )
11 8 9 10 mp2an 
 |-  R e. ( TopOn ` ( RR ^m ( 1 ... N ) ) )
12 11 topontopi 
 |-  R e. Top
13 reex 
 |-  RR e. _V
14 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
15 mapss 
 |-  ( ( RR e. _V /\ ( 0 [,] 1 ) C_ RR ) -> ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) C_ ( RR ^m ( 1 ... N ) ) )
16 13 14 15 mp2an 
 |-  ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) C_ ( RR ^m ( 1 ... N ) )
17 2 16 eqsstri 
 |-  I C_ ( RR ^m ( 1 ... N ) )
18 11 toponunii 
 |-  ( RR ^m ( 1 ... N ) ) = U. R
19 18 restuni 
 |-  ( ( R e. Top /\ I C_ ( RR ^m ( 1 ... N ) ) ) -> I = U. ( R |`t I ) )
20 12 17 19 mp2an 
 |-  I = U. ( R |`t I )
21 20 18 cnf 
 |-  ( F e. ( ( R |`t I ) Cn R ) -> F : I --> ( RR ^m ( 1 ... N ) ) )
22 4 21 syl 
 |-  ( ph -> F : I --> ( RR ^m ( 1 ... N ) ) )
23 22 ffvelrnda 
 |-  ( ( ph /\ c e. I ) -> ( F ` c ) e. ( RR ^m ( 1 ... N ) ) )
24 elmapi 
 |-  ( ( F ` c ) e. ( RR ^m ( 1 ... N ) ) -> ( F ` c ) : ( 1 ... N ) --> RR )
25 23 24 syl 
 |-  ( ( ph /\ c e. I ) -> ( F ` c ) : ( 1 ... N ) --> RR )
26 25 ffvelrnda 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` c ) ` n ) e. RR )
27 recn 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( ( F ` c ) ` n ) e. CC )
28 absrpcl 
 |-  ( ( ( ( F ` c ) ` n ) e. CC /\ ( ( F ` c ) ` n ) =/= 0 ) -> ( abs ` ( ( F ` c ) ` n ) ) e. RR+ )
29 28 ex 
 |-  ( ( ( F ` c ) ` n ) e. CC -> ( ( ( F ` c ) ` n ) =/= 0 -> ( abs ` ( ( F ` c ) ` n ) ) e. RR+ ) )
30 27 29 syl 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) =/= 0 -> ( abs ` ( ( F ` c ) ` n ) ) e. RR+ ) )
31 ltsubrp 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ ( abs ` ( ( F ` c ) ` n ) ) e. RR+ ) -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` c ) ` n ) )
32 ltaddrp 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ ( abs ` ( ( F ` c ) ` n ) ) e. RR+ ) -> ( ( F ` c ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) )
33 31 32 jca 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ ( abs ` ( ( F ` c ) ` n ) ) e. RR+ ) -> ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` c ) ` n ) /\ ( ( F ` c ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) )
34 33 ex 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( ( abs ` ( ( F ` c ) ` n ) ) e. RR+ -> ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` c ) ` n ) /\ ( ( F ` c ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
35 30 34 syld 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) =/= 0 -> ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` c ) ` n ) /\ ( ( F ` c ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
36 27 abscld 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( abs ` ( ( F ` c ) ` n ) ) e. RR )
37 resubcl 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ ( abs ` ( ( F ` c ) ` n ) ) e. RR ) -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) e. RR )
38 36 37 mpdan 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) e. RR )
39 38 rexrd 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) e. RR* )
40 readdcl 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ ( abs ` ( ( F ` c ) ` n ) ) e. RR ) -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) e. RR )
41 36 40 mpdan 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) e. RR )
42 41 rexrd 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) e. RR* )
43 rexr 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( ( F ` c ) ` n ) e. RR* )
44 elioo5 
 |-  ( ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) e. RR* /\ ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) e. RR* /\ ( ( F ` c ) ` n ) e. RR* ) -> ( ( ( F ` c ) ` n ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) <-> ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` c ) ` n ) /\ ( ( F ` c ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
45 39 42 43 44 syl3anc 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) <-> ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` c ) ` n ) /\ ( ( F ` c ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
46 35 45 sylibrd 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) =/= 0 -> ( ( F ` c ) ` n ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
47 26 46 syl 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) =/= 0 -> ( ( F ` c ) ` n ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
48 fveq2 
 |-  ( x = c -> ( F ` x ) = ( F ` c ) )
49 48 fveq1d 
 |-  ( x = c -> ( ( F ` x ) ` n ) = ( ( F ` c ) ` n ) )
50 eqid 
 |-  ( x e. I |-> ( ( F ` x ) ` n ) ) = ( x e. I |-> ( ( F ` x ) ` n ) )
51 fvex 
 |-  ( ( F ` c ) ` n ) e. _V
52 49 50 51 fvmpt 
 |-  ( c e. I -> ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) = ( ( F ` c ) ` n ) )
53 52 eleq1d 
 |-  ( c e. I -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) <-> ( ( F ` c ) ` n ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
54 53 ad2antlr 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) <-> ( ( F ` c ) ` n ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
55 47 54 sylibrd 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) =/= 0 -> ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
56 iooretop 
 |-  ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) e. ( topGen ` ran (,) )
57 resttopon 
 |-  ( ( R e. ( TopOn ` ( RR ^m ( 1 ... N ) ) ) /\ I C_ ( RR ^m ( 1 ... N ) ) ) -> ( R |`t I ) e. ( TopOn ` I ) )
58 11 17 57 mp2an 
 |-  ( R |`t I ) e. ( TopOn ` I )
59 58 a1i 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( R |`t I ) e. ( TopOn ` I ) )
60 22 feqmptd 
 |-  ( ph -> F = ( x e. I |-> ( F ` x ) ) )
61 60 4 eqeltrrd 
 |-  ( ph -> ( x e. I |-> ( F ` x ) ) e. ( ( R |`t I ) Cn R ) )
62 61 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. I |-> ( F ` x ) ) e. ( ( R |`t I ) Cn R ) )
63 11 a1i 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> R e. ( TopOn ` ( RR ^m ( 1 ... N ) ) ) )
64 retop 
 |-  ( topGen ` ran (,) ) e. Top
65 64 fconst6 
 |-  ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Top
66 18 3 ptpjcn 
 |-  ( ( ( 1 ... N ) e. _V /\ ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Top /\ n e. ( 1 ... N ) ) -> ( z e. ( RR ^m ( 1 ... N ) ) |-> ( z ` n ) ) e. ( R Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) )
67 8 65 66 mp3an12 
 |-  ( n e. ( 1 ... N ) -> ( z e. ( RR ^m ( 1 ... N ) ) |-> ( z ` n ) ) e. ( R Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) )
68 fvex 
 |-  ( topGen ` ran (,) ) e. _V
69 68 fvconst2 
 |-  ( n e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) = ( topGen ` ran (,) ) )
70 69 oveq2d 
 |-  ( n e. ( 1 ... N ) -> ( R Cn ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) ) = ( R Cn ( topGen ` ran (,) ) ) )
71 67 70 eleqtrd 
 |-  ( n e. ( 1 ... N ) -> ( z e. ( RR ^m ( 1 ... N ) ) |-> ( z ` n ) ) e. ( R Cn ( topGen ` ran (,) ) ) )
72 71 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( z e. ( RR ^m ( 1 ... N ) ) |-> ( z ` n ) ) e. ( R Cn ( topGen ` ran (,) ) ) )
73 fveq1 
 |-  ( z = ( F ` x ) -> ( z ` n ) = ( ( F ` x ) ` n ) )
74 59 62 63 72 73 cnmpt11 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( R |`t I ) Cn ( topGen ` ran (,) ) ) )
75 20 cncnpi 
 |-  ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( R |`t I ) Cn ( topGen ` ran (,) ) ) /\ c e. I ) -> ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( ( R |`t I ) CnP ( topGen ` ran (,) ) ) ` c ) )
76 74 75 sylan 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ c e. I ) -> ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( ( R |`t I ) CnP ( topGen ` ran (,) ) ) ` c ) )
77 76 an32s 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( ( R |`t I ) CnP ( topGen ` ran (,) ) ) ` c ) )
78 iscnp 
 |-  ( ( ( R |`t I ) e. ( TopOn ` I ) /\ ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ c e. I ) -> ( ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( ( R |`t I ) CnP ( topGen ` ran (,) ) ) ` c ) <-> ( ( x e. I |-> ( ( F ` x ) ` n ) ) : I --> RR /\ A. z e. ( topGen ` ran (,) ) ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. z -> E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) ) ) ) )
79 58 9 78 mp3an12 
 |-  ( c e. I -> ( ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( ( R |`t I ) CnP ( topGen ` ran (,) ) ) ` c ) <-> ( ( x e. I |-> ( ( F ` x ) ` n ) ) : I --> RR /\ A. z e. ( topGen ` ran (,) ) ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. z -> E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) ) ) ) )
80 79 ad2antlr 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( x e. I |-> ( ( F ` x ) ` n ) ) e. ( ( ( R |`t I ) CnP ( topGen ` ran (,) ) ) ` c ) <-> ( ( x e. I |-> ( ( F ` x ) ` n ) ) : I --> RR /\ A. z e. ( topGen ` ran (,) ) ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. z -> E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) ) ) ) )
81 77 80 mpbid 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( x e. I |-> ( ( F ` x ) ` n ) ) : I --> RR /\ A. z e. ( topGen ` ran (,) ) ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. z -> E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) ) ) )
82 81 simprd 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> A. z e. ( topGen ` ran (,) ) ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. z -> E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) ) )
83 eleq2 
 |-  ( z = ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. z <-> ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
84 sseq2 
 |-  ( z = ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z <-> ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
85 84 anbi2d 
 |-  ( z = ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> ( ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) <-> ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) ) )
86 85 rexbidv 
 |-  ( z = ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> ( E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) <-> E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) ) )
87 83 86 imbi12d 
 |-  ( z = ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> ( ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. z -> E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) ) <-> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) ) ) )
88 87 rspcv 
 |-  ( ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) e. ( topGen ` ran (,) ) -> ( A. z e. ( topGen ` ran (,) ) ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. z -> E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ z ) ) -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) ) ) )
89 56 82 88 mpsyl 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` c ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) ) )
90 55 89 syld 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) =/= 0 -> E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) ) )
91 0re 
 |-  0 e. RR
92 letric 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ 0 e. RR ) -> ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) )
93 26 91 92 sylancl 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) )
94 90 93 jctird 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) =/= 0 -> ( E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) ) )
95 r19.41v 
 |-  ( E. v e. ( R |`t I ) ( ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) <-> ( E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) )
96 anass 
 |-  ( ( ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) <-> ( c e. v /\ ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) ) )
97 96 rexbii 
 |-  ( E. v e. ( R |`t I ) ( ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) <-> E. v e. ( R |`t I ) ( c e. v /\ ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) ) )
98 95 97 bitr3i 
 |-  ( ( E. v e. ( R |`t I ) ( c e. v /\ ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) <-> E. v e. ( R |`t I ) ( c e. v /\ ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) ) )
99 94 98 syl6ib 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) =/= 0 -> E. v e. ( R |`t I ) ( c e. v /\ ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) ) ) )
100 58 topontopi 
 |-  ( R |`t I ) e. Top
101 20 eltopss 
 |-  ( ( ( R |`t I ) e. Top /\ v e. ( R |`t I ) ) -> v C_ I )
102 100 101 mpan 
 |-  ( v e. ( R |`t I ) -> v C_ I )
103 fvex 
 |-  ( ( F ` x ) ` n ) e. _V
104 103 50 dmmpti 
 |-  dom ( x e. I |-> ( ( F ` x ) ` n ) ) = I
105 104 sseq2i 
 |-  ( v C_ dom ( x e. I |-> ( ( F ` x ) ` n ) ) <-> v C_ I )
106 funmpt 
 |-  Fun ( x e. I |-> ( ( F ` x ) ` n ) )
107 funimass4 
 |-  ( ( Fun ( x e. I |-> ( ( F ` x ) ` n ) ) /\ v C_ dom ( x e. I |-> ( ( F ` x ) ` n ) ) ) -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) <-> A. z e. v ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` z ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
108 106 107 mpan 
 |-  ( v C_ dom ( x e. I |-> ( ( F ` x ) ` n ) ) -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) <-> A. z e. v ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` z ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
109 105 108 sylbir 
 |-  ( v C_ I -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) <-> A. z e. v ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` z ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
110 ssel2 
 |-  ( ( v C_ I /\ z e. v ) -> z e. I )
111 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
112 111 fveq1d 
 |-  ( x = z -> ( ( F ` x ) ` n ) = ( ( F ` z ) ` n ) )
113 fvex 
 |-  ( ( F ` z ) ` n ) e. _V
114 112 50 113 fvmpt 
 |-  ( z e. I -> ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` z ) = ( ( F ` z ) ` n ) )
115 114 eleq1d 
 |-  ( z e. I -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` z ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) <-> ( ( F ` z ) ` n ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
116 eliooord 
 |-  ( ( ( F ` z ) ` n ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) )
117 115 116 syl6bi 
 |-  ( z e. I -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` z ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
118 110 117 syl 
 |-  ( ( v C_ I /\ z e. v ) -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` z ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
119 118 ralimdva 
 |-  ( v C_ I -> ( A. z e. v ( ( x e. I |-> ( ( F ` x ) ` n ) ) ` z ) e. ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> A. z e. v ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
120 109 119 sylbid 
 |-  ( v C_ I -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> A. z e. v ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
121 120 adantl 
 |-  ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ v C_ I ) -> ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> A. z e. v ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) )
122 absnid 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ ( ( F ` c ) ` n ) <_ 0 ) -> ( abs ` ( ( F ` c ) ` n ) ) = -u ( ( F ` c ) ` n ) )
123 122 oveq2d 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ ( ( F ` c ) ` n ) <_ 0 ) -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) = ( ( ( F ` c ) ` n ) + -u ( ( F ` c ) ` n ) ) )
124 27 negidd 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) + -u ( ( F ` c ) ` n ) ) = 0 )
125 124 adantr 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ ( ( F ` c ) ` n ) <_ 0 ) -> ( ( ( F ` c ) ` n ) + -u ( ( F ` c ) ` n ) ) = 0 )
126 123 125 eqtrd 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ ( ( F ` c ) ` n ) <_ 0 ) -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) = 0 )
127 26 126 sylan 
 |-  ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ ( ( F ` c ) ` n ) <_ 0 ) -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) = 0 )
128 127 adantr 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ ( ( F ` c ) ` n ) <_ 0 ) /\ z e. I ) -> ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) = 0 )
129 128 breq2d 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ ( ( F ` c ) ` n ) <_ 0 ) /\ z e. I ) -> ( ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) <-> ( ( F ` z ) ` n ) < 0 ) )
130 22 ffvelrnda 
 |-  ( ( ph /\ z e. I ) -> ( F ` z ) e. ( RR ^m ( 1 ... N ) ) )
131 elmapi 
 |-  ( ( F ` z ) e. ( RR ^m ( 1 ... N ) ) -> ( F ` z ) : ( 1 ... N ) --> RR )
132 130 131 syl 
 |-  ( ( ph /\ z e. I ) -> ( F ` z ) : ( 1 ... N ) --> RR )
133 132 ffvelrnda 
 |-  ( ( ( ph /\ z e. I ) /\ n e. ( 1 ... N ) ) -> ( ( F ` z ) ` n ) e. RR )
134 133 an32s 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ z e. I ) -> ( ( F ` z ) ` n ) e. RR )
135 0red 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ z e. I ) -> 0 e. RR )
136 134 135 ltnled 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ z e. I ) -> ( ( ( F ` z ) ` n ) < 0 <-> -. 0 <_ ( ( F ` z ) ` n ) ) )
137 136 adantllr 
 |-  ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ z e. I ) -> ( ( ( F ` z ) ` n ) < 0 <-> -. 0 <_ ( ( F ` z ) ` n ) ) )
138 137 adantlr 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ ( ( F ` c ) ` n ) <_ 0 ) /\ z e. I ) -> ( ( ( F ` z ) ` n ) < 0 <-> -. 0 <_ ( ( F ` z ) ` n ) ) )
139 129 138 bitrd 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ ( ( F ` c ) ` n ) <_ 0 ) /\ z e. I ) -> ( ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) <-> -. 0 <_ ( ( F ` z ) ` n ) ) )
140 139 biimpd 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ ( ( F ` c ) ` n ) <_ 0 ) /\ z e. I ) -> ( ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) -> -. 0 <_ ( ( F ` z ) ` n ) ) )
141 110 140 sylan2 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ ( ( F ` c ) ` n ) <_ 0 ) /\ ( v C_ I /\ z e. v ) ) -> ( ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) -> -. 0 <_ ( ( F ` z ) ` n ) ) )
142 141 anassrs 
 |-  ( ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ ( ( F ` c ) ` n ) <_ 0 ) /\ v C_ I ) /\ z e. v ) -> ( ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) -> -. 0 <_ ( ( F ` z ) ` n ) ) )
143 142 adantld 
 |-  ( ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ ( ( F ` c ) ` n ) <_ 0 ) /\ v C_ I ) /\ z e. v ) -> ( ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> -. 0 <_ ( ( F ` z ) ` n ) ) )
144 143 ralimdva 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ ( ( F ` c ) ` n ) <_ 0 ) /\ v C_ I ) -> ( A. z e. v ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> A. z e. v -. 0 <_ ( ( F ` z ) ` n ) ) )
145 144 an32s 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ v C_ I ) /\ ( ( F ` c ) ` n ) <_ 0 ) -> ( A. z e. v ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> A. z e. v -. 0 <_ ( ( F ` z ) ` n ) ) )
146 145 impancom 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ v C_ I ) /\ A. z e. v ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) -> ( ( ( F ` c ) ` n ) <_ 0 -> A. z e. v -. 0 <_ ( ( F ` z ) ` n ) ) )
147 absid 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ 0 <_ ( ( F ` c ) ` n ) ) -> ( abs ` ( ( F ` c ) ` n ) ) = ( ( F ` c ) ` n ) )
148 147 oveq2d 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ 0 <_ ( ( F ` c ) ` n ) ) -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) = ( ( ( F ` c ) ` n ) - ( ( F ` c ) ` n ) ) )
149 27 subidd 
 |-  ( ( ( F ` c ) ` n ) e. RR -> ( ( ( F ` c ) ` n ) - ( ( F ` c ) ` n ) ) = 0 )
150 149 adantr 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ 0 <_ ( ( F ` c ) ` n ) ) -> ( ( ( F ` c ) ` n ) - ( ( F ` c ) ` n ) ) = 0 )
151 148 150 eqtrd 
 |-  ( ( ( ( F ` c ) ` n ) e. RR /\ 0 <_ ( ( F ` c ) ` n ) ) -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) = 0 )
152 26 151 sylan 
 |-  ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ 0 <_ ( ( F ` c ) ` n ) ) -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) = 0 )
153 152 adantr 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ 0 <_ ( ( F ` c ) ` n ) ) /\ z e. I ) -> ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) = 0 )
154 153 breq1d 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ 0 <_ ( ( F ` c ) ` n ) ) /\ z e. I ) -> ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) <-> 0 < ( ( F ` z ) ` n ) ) )
155 135 134 ltnled 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ z e. I ) -> ( 0 < ( ( F ` z ) ` n ) <-> -. ( ( F ` z ) ` n ) <_ 0 ) )
156 155 adantllr 
 |-  ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ z e. I ) -> ( 0 < ( ( F ` z ) ` n ) <-> -. ( ( F ` z ) ` n ) <_ 0 ) )
157 156 adantlr 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ 0 <_ ( ( F ` c ) ` n ) ) /\ z e. I ) -> ( 0 < ( ( F ` z ) ` n ) <-> -. ( ( F ` z ) ` n ) <_ 0 ) )
158 154 157 bitrd 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ 0 <_ ( ( F ` c ) ` n ) ) /\ z e. I ) -> ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) <-> -. ( ( F ` z ) ` n ) <_ 0 ) )
159 158 biimpd 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ 0 <_ ( ( F ` c ) ` n ) ) /\ z e. I ) -> ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) -> -. ( ( F ` z ) ` n ) <_ 0 ) )
160 110 159 sylan2 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ 0 <_ ( ( F ` c ) ` n ) ) /\ ( v C_ I /\ z e. v ) ) -> ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) -> -. ( ( F ` z ) ` n ) <_ 0 ) )
161 160 anassrs 
 |-  ( ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ 0 <_ ( ( F ` c ) ` n ) ) /\ v C_ I ) /\ z e. v ) -> ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) -> -. ( ( F ` z ) ` n ) <_ 0 ) )
162 161 adantrd 
 |-  ( ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ 0 <_ ( ( F ` c ) ` n ) ) /\ v C_ I ) /\ z e. v ) -> ( ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> -. ( ( F ` z ) ` n ) <_ 0 ) )
163 162 ralimdva 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ 0 <_ ( ( F ` c ) ` n ) ) /\ v C_ I ) -> ( A. z e. v ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) )
164 163 an32s 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ v C_ I ) /\ 0 <_ ( ( F ` c ) ` n ) ) -> ( A. z e. v ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) -> A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) )
165 164 impancom 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ v C_ I ) /\ A. z e. v ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) -> ( 0 <_ ( ( F ` c ) ` n ) -> A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) )
166 146 165 orim12d 
 |-  ( ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ v C_ I ) /\ A. z e. v ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) ) -> ( ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) -> ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) )
167 166 expimpd 
 |-  ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ v C_ I ) -> ( ( A. z e. v ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) < ( ( F ` z ) ` n ) /\ ( ( F ` z ) ` n ) < ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) -> ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) )
168 121 167 syland 
 |-  ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ v C_ I ) -> ( ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) -> ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) )
169 102 168 sylan2 
 |-  ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ v e. ( R |`t I ) ) -> ( ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) -> ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) )
170 169 anim2d 
 |-  ( ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) /\ v e. ( R |`t I ) ) -> ( ( c e. v /\ ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) ) -> ( c e. v /\ ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) ) )
171 170 reximdva 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( E. v e. ( R |`t I ) ( c e. v /\ ( ( ( x e. I |-> ( ( F ` x ) ` n ) ) " v ) C_ ( ( ( ( F ` c ) ` n ) - ( abs ` ( ( F ` c ) ` n ) ) ) (,) ( ( ( F ` c ) ` n ) + ( abs ` ( ( F ` c ) ` n ) ) ) ) /\ ( ( ( F ` c ) ` n ) <_ 0 \/ 0 <_ ( ( F ` c ) ` n ) ) ) ) -> E. v e. ( R |`t I ) ( c e. v /\ ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) ) )
172 99 171 syld 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) =/= 0 -> E. v e. ( R |`t I ) ( c e. v /\ ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) ) )
173 ralnex 
 |-  ( A. z e. v -. 0 r ( ( F ` z ) ` n ) <-> -. E. z e. v 0 r ( ( F ` z ) ` n ) )
174 173 rexbii 
 |-  ( E. r e. { <_ , `' <_ } A. z e. v -. 0 r ( ( F ` z ) ` n ) <-> E. r e. { <_ , `' <_ } -. E. z e. v 0 r ( ( F ` z ) ` n ) )
175 letsr 
 |-  <_ e. TosetRel
176 175 elexi 
 |-  <_ e. _V
177 176 cnvex 
 |-  `' <_ e. _V
178 breq 
 |-  ( r = <_ -> ( 0 r ( ( F ` z ) ` n ) <-> 0 <_ ( ( F ` z ) ` n ) ) )
179 178 notbid 
 |-  ( r = <_ -> ( -. 0 r ( ( F ` z ) ` n ) <-> -. 0 <_ ( ( F ` z ) ` n ) ) )
180 179 ralbidv 
 |-  ( r = <_ -> ( A. z e. v -. 0 r ( ( F ` z ) ` n ) <-> A. z e. v -. 0 <_ ( ( F ` z ) ` n ) ) )
181 breq 
 |-  ( r = `' <_ -> ( 0 r ( ( F ` z ) ` n ) <-> 0 `' <_ ( ( F ` z ) ` n ) ) )
182 c0ex 
 |-  0 e. _V
183 182 113 brcnv 
 |-  ( 0 `' <_ ( ( F ` z ) ` n ) <-> ( ( F ` z ) ` n ) <_ 0 )
184 181 183 syl6bb 
 |-  ( r = `' <_ -> ( 0 r ( ( F ` z ) ` n ) <-> ( ( F ` z ) ` n ) <_ 0 ) )
185 184 notbid 
 |-  ( r = `' <_ -> ( -. 0 r ( ( F ` z ) ` n ) <-> -. ( ( F ` z ) ` n ) <_ 0 ) )
186 185 ralbidv 
 |-  ( r = `' <_ -> ( A. z e. v -. 0 r ( ( F ` z ) ` n ) <-> A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) )
187 176 177 180 186 rexpr 
 |-  ( E. r e. { <_ , `' <_ } A. z e. v -. 0 r ( ( F ` z ) ` n ) <-> ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) )
188 rexnal 
 |-  ( E. r e. { <_ , `' <_ } -. E. z e. v 0 r ( ( F ` z ) ` n ) <-> -. A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) )
189 174 187 188 3bitr3i 
 |-  ( ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) <-> -. A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) )
190 189 anbi2i 
 |-  ( ( c e. v /\ ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) <-> ( c e. v /\ -. A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
191 annim 
 |-  ( ( c e. v /\ -. A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) <-> -. ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
192 190 191 bitri 
 |-  ( ( c e. v /\ ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) <-> -. ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
193 192 rexbii 
 |-  ( E. v e. ( R |`t I ) ( c e. v /\ ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) <-> E. v e. ( R |`t I ) -. ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
194 rexnal 
 |-  ( E. v e. ( R |`t I ) -. ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) <-> -. A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
195 193 194 bitri 
 |-  ( E. v e. ( R |`t I ) ( c e. v /\ ( A. z e. v -. 0 <_ ( ( F ` z ) ` n ) \/ A. z e. v -. ( ( F ` z ) ` n ) <_ 0 ) ) <-> -. A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
196 172 195 syl6ib 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( ( ( F ` c ) ` n ) =/= 0 -> -. A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) )
197 196 necon4ad 
 |-  ( ( ( ph /\ c e. I ) /\ n e. ( 1 ... N ) ) -> ( A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) -> ( ( F ` c ) ` n ) = 0 ) )
198 197 ralimdva 
 |-  ( ( ph /\ c e. I ) -> ( A. n e. ( 1 ... N ) A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) -> A. n e. ( 1 ... N ) ( ( F ` c ) ` n ) = 0 ) )
199 25 ffnd 
 |-  ( ( ph /\ c e. I ) -> ( F ` c ) Fn ( 1 ... N ) )
200 198 199 jctild 
 |-  ( ( ph /\ c e. I ) -> ( A. n e. ( 1 ... N ) A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) -> ( ( F ` c ) Fn ( 1 ... N ) /\ A. n e. ( 1 ... N ) ( ( F ` c ) ` n ) = 0 ) ) )
201 fconstfv 
 |-  ( ( F ` c ) : ( 1 ... N ) --> { 0 } <-> ( ( F ` c ) Fn ( 1 ... N ) /\ A. n e. ( 1 ... N ) ( ( F ` c ) ` n ) = 0 ) )
202 182 fconst2 
 |-  ( ( F ` c ) : ( 1 ... N ) --> { 0 } <-> ( F ` c ) = ( ( 1 ... N ) X. { 0 } ) )
203 201 202 bitr3i 
 |-  ( ( ( F ` c ) Fn ( 1 ... N ) /\ A. n e. ( 1 ... N ) ( ( F ` c ) ` n ) = 0 ) <-> ( F ` c ) = ( ( 1 ... N ) X. { 0 } ) )
204 200 203 syl6ib 
 |-  ( ( ph /\ c e. I ) -> ( A. n e. ( 1 ... N ) A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) -> ( F ` c ) = ( ( 1 ... N ) X. { 0 } ) ) )
205 204 reximdva 
 |-  ( ph -> ( E. c e. I A. n e. ( 1 ... N ) A. v e. ( R |`t I ) ( c e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) -> E. c e. I ( F ` c ) = ( ( 1 ... N ) X. { 0 } ) ) )
206 7 205 mpd 
 |-  ( ph -> E. c e. I ( F ` c ) = ( ( 1 ... N ) X. { 0 } ) )