Metamath Proof Explorer

Theorem poimirlem32

Description: Lemma for poimir , combining poimirlem28 , poimirlem30 , and poimirlem31 to get Equation (1) of 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 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 ) ) )

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 adantr 
 |-  ( ( ph /\ k e. NN ) -> N e. NN )
8 fvoveq1 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) = ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) )
9 8 fveq1d 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) = ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) )
10 9 breq2d 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) <-> 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) ) )
11 fveq1 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( p ` b ) = ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) )
12 11 neeq1d 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( ( p ` b ) =/= 0 <-> ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) )
13 10 12 anbi12d 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) <-> ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) ) )
14 13 ralbidv 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) <-> A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) ) )
15 14 rabbidv 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } = { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } )
16 15 uneq2d 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) = ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) )
17 16 supeq1d 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) )
18 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
19 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
20 18 19 syl 
 |-  ( ph -> 0 e. ( 0 ... N ) )
21 20 snssd 
 |-  ( ph -> { 0 } C_ ( 0 ... N ) )
22 ssrab2 
 |-  { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } C_ ( 1 ... N )
23 fz1ssfz0 
 |-  ( 1 ... N ) C_ ( 0 ... N )
24 22 23 sstri 
 |-  { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } C_ ( 0 ... N )
25 24 a1i 
 |-  ( ph -> { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } C_ ( 0 ... N ) )
26 21 25 unssd 
 |-  ( ph -> ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) C_ ( 0 ... N ) )
27 ltso 
 |-  < Or RR
28 snfi 
 |-  { 0 } e. Fin
29 fzfi 
 |-  ( 1 ... N ) e. Fin
30 rabfi 
 |-  ( ( 1 ... N ) e. Fin -> { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } e. Fin )
31 29 30 ax-mp 
 |-  { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } e. Fin
32 unfi 
 |-  ( ( { 0 } e. Fin /\ { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } e. Fin ) -> ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) e. Fin )
33 28 31 32 mp2an 
 |-  ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) e. Fin
34 c0ex 
 |-  0 e. _V
35 34 snid 
 |-  0 e. { 0 }
36 elun1 
 |-  ( 0 e. { 0 } -> 0 e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) )
37 ne0i 
 |-  ( 0 e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) -> ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) =/= (/) )
38 35 36 37 mp2b 
 |-  ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) =/= (/)
39 0red 
 |-  ( ( ph -> N e. NN ) -> 0 e. RR )
40 39 snssd 
 |-  ( ( ph -> N e. NN ) -> { 0 } C_ RR )
41 1 40 ax-mp 
 |-  { 0 } C_ RR
42 elfzelz 
 |-  ( n e. ( 1 ... N ) -> n e. ZZ )
43 42 ssriv 
 |-  ( 1 ... N ) C_ ZZ
44 zssre 
 |-  ZZ C_ RR
45 43 44 sstri 
 |-  ( 1 ... N ) C_ RR
46 22 45 sstri 
 |-  { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } C_ RR
47 41 46 unssi 
 |-  ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) C_ RR
48 33 38 47 3pm3.2i 
 |-  ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) e. Fin /\ ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) =/= (/) /\ ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) C_ RR )
49 fisupcl 
 |-  ( ( < Or RR /\ ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) e. Fin /\ ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) =/= (/) /\ ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) C_ RR ) ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) )
50 27 48 49 mp2an 
 |-  sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } )
51 ssel 
 |-  ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) C_ ( 0 ... N ) -> ( sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) e. ( 0 ... N ) ) )
52 26 50 51 mpisyl 
 |-  ( ph -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) e. ( 0 ... N ) )
53 52 ad2antrr 
 |-  ( ( ( ph /\ k e. NN ) /\ p : ( 1 ... N ) --> ( 0 ... k ) ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) e. ( 0 ... N ) )
54 elfznn 
 |-  ( n e. ( 1 ... N ) -> n e. NN )
55 nngt0 
 |-  ( n e. NN -> 0 < n )
56 55 adantr 
 |-  ( ( n e. NN /\ ( p ` n ) = 0 ) -> 0 < n )
57 simpr 
 |-  ( ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> ( p ` b ) =/= 0 )
58 57 ralimi 
 |-  ( A. b e. ( 1 ... s ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> A. b e. ( 1 ... s ) ( p ` b ) =/= 0 )
59 elfznn 
 |-  ( s e. ( 1 ... N ) -> s e. NN )
60 nnre 
 |-  ( n e. NN -> n e. RR )
61 nnre 
 |-  ( s e. NN -> s e. RR )
62 lenlt 
 |-  ( ( n e. RR /\ s e. RR ) -> ( n <_ s <-> -. s < n ) )
63 60 61 62 syl2an 
 |-  ( ( n e. NN /\ s e. NN ) -> ( n <_ s <-> -. s < n ) )
64 elfz1b 
 |-  ( n e. ( 1 ... s ) <-> ( n e. NN /\ s e. NN /\ n <_ s ) )
65 64 biimpri 
 |-  ( ( n e. NN /\ s e. NN /\ n <_ s ) -> n e. ( 1 ... s ) )
66 65 3expia 
 |-  ( ( n e. NN /\ s e. NN ) -> ( n <_ s -> n e. ( 1 ... s ) ) )
67 63 66 sylbird 
 |-  ( ( n e. NN /\ s e. NN ) -> ( -. s < n -> n e. ( 1 ... s ) ) )
68 fveq2 
 |-  ( b = n -> ( p ` b ) = ( p ` n ) )
69 68 eqeq1d 
 |-  ( b = n -> ( ( p ` b ) = 0 <-> ( p ` n ) = 0 ) )
70 69 rspcev 
 |-  ( ( n e. ( 1 ... s ) /\ ( p ` n ) = 0 ) -> E. b e. ( 1 ... s ) ( p ` b ) = 0 )
71 70 expcom 
 |-  ( ( p ` n ) = 0 -> ( n e. ( 1 ... s ) -> E. b e. ( 1 ... s ) ( p ` b ) = 0 ) )
72 67 71 sylan9 
 |-  ( ( ( n e. NN /\ s e. NN ) /\ ( p ` n ) = 0 ) -> ( -. s < n -> E. b e. ( 1 ... s ) ( p ` b ) = 0 ) )
73 72 an32s 
 |-  ( ( ( n e. NN /\ ( p ` n ) = 0 ) /\ s e. NN ) -> ( -. s < n -> E. b e. ( 1 ... s ) ( p ` b ) = 0 ) )
74 nne 
 |-  ( -. ( p ` b ) =/= 0 <-> ( p ` b ) = 0 )
75 74 rexbii 
 |-  ( E. b e. ( 1 ... s ) -. ( p ` b ) =/= 0 <-> E. b e. ( 1 ... s ) ( p ` b ) = 0 )
76 rexnal 
 |-  ( E. b e. ( 1 ... s ) -. ( p ` b ) =/= 0 <-> -. A. b e. ( 1 ... s ) ( p ` b ) =/= 0 )
77 75 76 bitr3i 
 |-  ( E. b e. ( 1 ... s ) ( p ` b ) = 0 <-> -. A. b e. ( 1 ... s ) ( p ` b ) =/= 0 )
78 73 77 imbitrdi 
 |-  ( ( ( n e. NN /\ ( p ` n ) = 0 ) /\ s e. NN ) -> ( -. s < n -> -. A. b e. ( 1 ... s ) ( p ` b ) =/= 0 ) )
79 78 con4d 
 |-  ( ( ( n e. NN /\ ( p ` n ) = 0 ) /\ s e. NN ) -> ( A. b e. ( 1 ... s ) ( p ` b ) =/= 0 -> s < n ) )
80 59 79 sylan2 
 |-  ( ( ( n e. NN /\ ( p ` n ) = 0 ) /\ s e. ( 1 ... N ) ) -> ( A. b e. ( 1 ... s ) ( p ` b ) =/= 0 -> s < n ) )
81 58 80 syl5 
 |-  ( ( ( n e. NN /\ ( p ` n ) = 0 ) /\ s e. ( 1 ... N ) ) -> ( A. b e. ( 1 ... s ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> s < n ) )
82 81 ralrimiva 
 |-  ( ( n e. NN /\ ( p ` n ) = 0 ) -> A. s e. ( 1 ... N ) ( A. b e. ( 1 ... s ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> s < n ) )
83 ralunb 
 |-  ( A. s e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) s < n <-> ( A. s e. { 0 } s < n /\ A. s e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } s < n ) )
84 breq1 
 |-  ( s = 0 -> ( s < n <-> 0 < n ) )
85 34 84 ralsn 
 |-  ( A. s e. { 0 } s < n <-> 0 < n )
86 oveq2 
 |-  ( a = s -> ( 1 ... a ) = ( 1 ... s ) )
87 86 raleqdv 
 |-  ( a = s -> ( A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) <-> A. b e. ( 1 ... s ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) )
88 87 ralrab 
 |-  ( A. s e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } s < n <-> A. s e. ( 1 ... N ) ( A. b e. ( 1 ... s ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> s < n ) )
89 85 88 anbi12i 
 |-  ( ( A. s e. { 0 } s < n /\ A. s e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } s < n ) <-> ( 0 < n /\ A. s e. ( 1 ... N ) ( A. b e. ( 1 ... s ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> s < n ) ) )
90 83 89 bitri 
 |-  ( A. s e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) s < n <-> ( 0 < n /\ A. s e. ( 1 ... N ) ( A. b e. ( 1 ... s ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> s < n ) ) )
91 56 82 90 sylanbrc 
 |-  ( ( n e. NN /\ ( p ` n ) = 0 ) -> A. s e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) s < n )
92 breq1 
 |-  ( s = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) -> ( s < n <-> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) < n ) )
93 92 rspcva 
 |-  ( ( sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) /\ A. s e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) s < n ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) < n )
94 50 91 93 sylancr 
 |-  ( ( n e. NN /\ ( p ` n ) = 0 ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) < n )
95 54 94 sylan 
 |-  ( ( n e. ( 1 ... N ) /\ ( p ` n ) = 0 ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) < n )
96 95 3adant2 
 |-  ( ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = 0 ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) < n )
97 96 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = 0 ) ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) < n )
98 42 zred 
 |-  ( n e. ( 1 ... N ) -> n e. RR )
99 98 3ad2ant1 
 |-  ( ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) -> n e. RR )
100 99 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> n e. RR )
101 simpr1 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> n e. ( 1 ... N ) )
102 simpll 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> ph )
103 simplr 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) ) ) -> k e. NN )
104 elfzelz 
 |-  ( i e. ( 0 ... k ) -> i e. ZZ )
105 104 zred 
 |-  ( i e. ( 0 ... k ) -> i e. RR )
106 nndivre 
 |-  ( ( i e. RR /\ k e. NN ) -> ( i / k ) e. RR )
107 105 106 sylan 
 |-  ( ( i e. ( 0 ... k ) /\ k e. NN ) -> ( i / k ) e. RR )
108 elfzle1 
 |-  ( i e. ( 0 ... k ) -> 0 <_ i )
109 105 108 jca 
 |-  ( i e. ( 0 ... k ) -> ( i e. RR /\ 0 <_ i ) )
110 nnrp 
 |-  ( k e. NN -> k e. RR+ )
111 110 rpregt0d 
 |-  ( k e. NN -> ( k e. RR /\ 0 < k ) )
112 divge0 
 |-  ( ( ( i e. RR /\ 0 <_ i ) /\ ( k e. RR /\ 0 < k ) ) -> 0 <_ ( i / k ) )
113 109 111 112 syl2an 
 |-  ( ( i e. ( 0 ... k ) /\ k e. NN ) -> 0 <_ ( i / k ) )
114 elfzle2 
 |-  ( i e. ( 0 ... k ) -> i <_ k )
115 114 adantr 
 |-  ( ( i e. ( 0 ... k ) /\ k e. NN ) -> i <_ k )
116 105 adantr 
 |-  ( ( i e. ( 0 ... k ) /\ k e. NN ) -> i e. RR )
117 1red 
 |-  ( ( i e. ( 0 ... k ) /\ k e. NN ) -> 1 e. RR )
118 110 adantl 
 |-  ( ( i e. ( 0 ... k ) /\ k e. NN ) -> k e. RR+ )
119 116 117 118 ledivmuld 
 |-  ( ( i e. ( 0 ... k ) /\ k e. NN ) -> ( ( i / k ) <_ 1 <-> i <_ ( k x. 1 ) ) )
120 nncn 
 |-  ( k e. NN -> k e. CC )
121 120 mulridd 
 |-  ( k e. NN -> ( k x. 1 ) = k )
122 121 breq2d 
 |-  ( k e. NN -> ( i <_ ( k x. 1 ) <-> i <_ k ) )
123 122 adantl 
 |-  ( ( i e. ( 0 ... k ) /\ k e. NN ) -> ( i <_ ( k x. 1 ) <-> i <_ k ) )
124 119 123 bitrd 
 |-  ( ( i e. ( 0 ... k ) /\ k e. NN ) -> ( ( i / k ) <_ 1 <-> i <_ k ) )
125 115 124 mpbird 
 |-  ( ( i e. ( 0 ... k ) /\ k e. NN ) -> ( i / k ) <_ 1 )
126 elicc01 
 |-  ( ( i / k ) e. ( 0 [,] 1 ) <-> ( ( i / k ) e. RR /\ 0 <_ ( i / k ) /\ ( i / k ) <_ 1 ) )
127 107 113 125 126 syl3anbrc 
 |-  ( ( i e. ( 0 ... k ) /\ k e. NN ) -> ( i / k ) e. ( 0 [,] 1 ) )
128 127 ancoms 
 |-  ( ( k e. NN /\ i e. ( 0 ... k ) ) -> ( i / k ) e. ( 0 [,] 1 ) )
129 elsni 
 |-  ( j e. { k } -> j = k )
130 129 oveq2d 
 |-  ( j e. { k } -> ( i / j ) = ( i / k ) )
131 130 eleq1d 
 |-  ( j e. { k } -> ( ( i / j ) e. ( 0 [,] 1 ) <-> ( i / k ) e. ( 0 [,] 1 ) ) )
132 128 131 syl5ibrcom 
 |-  ( ( k e. NN /\ i e. ( 0 ... k ) ) -> ( j e. { k } -> ( i / j ) e. ( 0 [,] 1 ) ) )
133 132 impr 
 |-  ( ( k e. NN /\ ( i e. ( 0 ... k ) /\ j e. { k } ) ) -> ( i / j ) e. ( 0 [,] 1 ) )
134 103 133 sylan 
 |-  ( ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) ) ) /\ ( i e. ( 0 ... k ) /\ j e. { k } ) ) -> ( i / j ) e. ( 0 [,] 1 ) )
135 simprr 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) ) ) -> p : ( 1 ... N ) --> ( 0 ... k ) )
136 vex 
 |-  k e. _V
137 136 fconst 
 |-  ( ( 1 ... N ) X. { k } ) : ( 1 ... N ) --> { k }
138 137 a1i 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) ) ) -> ( ( 1 ... N ) X. { k } ) : ( 1 ... N ) --> { k } )
139 fzfid 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) ) ) -> ( 1 ... N ) e. Fin )
140 inidm 
 |-  ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
141 134 135 138 139 139 140 off 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) ) ) -> ( p oF / ( ( 1 ... N ) X. { k } ) ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
142 2 eleq2i 
 |-  ( ( p oF / ( ( 1 ... N ) X. { k } ) ) e. I <-> ( p oF / ( ( 1 ... N ) X. { k } ) ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) )
143 ovex 
 |-  ( 0 [,] 1 ) e. _V
144 ovex 
 |-  ( 1 ... N ) e. _V
145 143 144 elmap 
 |-  ( ( p oF / ( ( 1 ... N ) X. { k } ) ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) <-> ( p oF / ( ( 1 ... N ) X. { k } ) ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
146 142 145 bitri 
 |-  ( ( p oF / ( ( 1 ... N ) X. { k } ) ) e. I <-> ( p oF / ( ( 1 ... N ) X. { k } ) ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
147 141 146 sylibr 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) ) ) -> ( p oF / ( ( 1 ... N ) X. { k } ) ) e. I )
148 147 3adantr3 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> ( p oF / ( ( 1 ... N ) X. { k } ) ) e. I )
149 3anass 
 |-  ( ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) <-> ( n e. ( 1 ... N ) /\ ( p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) )
150 ancom 
 |-  ( ( n e. ( 1 ... N ) /\ ( p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) <-> ( ( p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) /\ n e. ( 1 ... N ) ) )
151 149 150 bitri 
 |-  ( ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) <-> ( ( p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) /\ n e. ( 1 ... N ) ) )
152 ffn 
 |-  ( p : ( 1 ... N ) --> ( 0 ... k ) -> p Fn ( 1 ... N ) )
153 152 ad2antrl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> p Fn ( 1 ... N ) )
154 fnconstg 
 |-  ( k e. _V -> ( ( 1 ... N ) X. { k } ) Fn ( 1 ... N ) )
155 136 154 mp1i 
 |-  ( ( ( ph /\ k e. NN ) /\ ( p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> ( ( 1 ... N ) X. { k } ) Fn ( 1 ... N ) )
156 fzfid 
 |-  ( ( ( ph /\ k e. NN ) /\ ( p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> ( 1 ... N ) e. Fin )
157 simplrr 
 |-  ( ( ( ( ph /\ k e. NN ) /\ ( p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) /\ n e. ( 1 ... N ) ) -> ( p ` n ) = k )
158 136 fvconst2 
 |-  ( n e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { k } ) ` n ) = k )
159 158 adantl 
 |-  ( ( ( ( ph /\ k e. NN ) /\ ( p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( 1 ... N ) X. { k } ) ` n ) = k )
160 153 155 156 156 140 157 159 ofval 
 |-  ( ( ( ( ph /\ k e. NN ) /\ ( p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) /\ n e. ( 1 ... N ) ) -> ( ( p oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = ( k / k ) )
161 160 anasss 
 |-  ( ( ( ph /\ k e. NN ) /\ ( ( p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) /\ n e. ( 1 ... N ) ) ) -> ( ( p oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = ( k / k ) )
162 151 161 sylan2b 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> ( ( p oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = ( k / k ) )
163 nnne0 
 |-  ( k e. NN -> k =/= 0 )
164 120 163 dividd 
 |-  ( k e. NN -> ( k / k ) = 1 )
165 164 ad2antlr 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> ( k / k ) = 1 )
166 162 165 eqtrd 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> ( ( p oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 1 )
167 ovex 
 |-  ( p oF / ( ( 1 ... N ) X. { k } ) ) e. _V
168 eleq1 
 |-  ( z = ( p oF / ( ( 1 ... N ) X. { k } ) ) -> ( z e. I <-> ( p oF / ( ( 1 ... N ) X. { k } ) ) e. I ) )
169 fveq1 
 |-  ( z = ( p oF / ( ( 1 ... N ) X. { k } ) ) -> ( z ` n ) = ( ( p oF / ( ( 1 ... N ) X. { k } ) ) ` n ) )
170 169 eqeq1d 
 |-  ( z = ( p oF / ( ( 1 ... N ) X. { k } ) ) -> ( ( z ` n ) = 1 <-> ( ( p oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 1 ) )
171 168 170 3anbi23d 
 |-  ( z = ( p oF / ( ( 1 ... N ) X. { k } ) ) -> ( ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 1 ) <-> ( n e. ( 1 ... N ) /\ ( p oF / ( ( 1 ... N ) X. { k } ) ) e. I /\ ( ( p oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 1 ) ) )
172 171 anbi2d 
 |-  ( z = ( p oF / ( ( 1 ... N ) X. { k } ) ) -> ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 1 ) ) <-> ( ph /\ ( n e. ( 1 ... N ) /\ ( p oF / ( ( 1 ... N ) X. { k } ) ) e. I /\ ( ( p oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 1 ) ) ) )
173 fveq2 
 |-  ( z = ( p oF / ( ( 1 ... N ) X. { k } ) ) -> ( F ` z ) = ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) )
174 173 fveq1d 
 |-  ( z = ( p oF / ( ( 1 ... N ) X. { k } ) ) -> ( ( F ` z ) ` n ) = ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) )
175 174 breq2d 
 |-  ( z = ( p oF / ( ( 1 ... N ) X. { k } ) ) -> ( 0 <_ ( ( F ` z ) ` n ) <-> 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
176 172 175 imbi12d 
 |-  ( z = ( p oF / ( ( 1 ... N ) X. { k } ) ) -> ( ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 1 ) ) -> 0 <_ ( ( F ` z ) ` n ) ) <-> ( ( ph /\ ( n e. ( 1 ... N ) /\ ( p oF / ( ( 1 ... N ) X. { k } ) ) e. I /\ ( ( p oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 1 ) ) -> 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) ) )
177 167 176 6 vtocl 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ ( p oF / ( ( 1 ... N ) X. { k } ) ) e. I /\ ( ( p oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 1 ) ) -> 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) )
178 102 101 148 166 177 syl13anc 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) )
179 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
180 simp3 
 |-  ( ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) -> ( p ` n ) = k )
181 neeq1 
 |-  ( ( p ` n ) = k -> ( ( p ` n ) =/= 0 <-> k =/= 0 ) )
182 163 181 syl5ibrcom 
 |-  ( k e. NN -> ( ( p ` n ) = k -> ( p ` n ) =/= 0 ) )
183 182 imp 
 |-  ( ( k e. NN /\ ( p ` n ) = k ) -> ( p ` n ) =/= 0 )
184 179 180 183 syl2an 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> ( p ` n ) =/= 0 )
185 vex 
 |-  n e. _V
186 fveq2 
 |-  ( b = n -> ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) = ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) )
187 186 breq2d 
 |-  ( b = n -> ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) <-> 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
188 68 neeq1d 
 |-  ( b = n -> ( ( p ` b ) =/= 0 <-> ( p ` n ) =/= 0 ) )
189 187 188 anbi12d 
 |-  ( b = n -> ( ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) <-> ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) /\ ( p ` n ) =/= 0 ) ) )
190 185 189 ralsn 
 |-  ( A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) <-> ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) /\ ( p ` n ) =/= 0 ) )
191 178 184 190 sylanbrc 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) )
192 42 zcnd 
 |-  ( n e. ( 1 ... N ) -> n e. CC )
193 1cnd 
 |-  ( n e. ( 1 ... N ) -> 1 e. CC )
194 192 193 subeq0ad 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) = 0 <-> n = 1 ) )
195 194 biimpcd 
 |-  ( ( n - 1 ) = 0 -> ( n e. ( 1 ... N ) -> n = 1 ) )
196 1z 
 |-  1 e. ZZ
197 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
198 196 197 ax-mp 
 |-  ( 1 ... 1 ) = { 1 }
199 oveq2 
 |-  ( n = 1 -> ( 1 ... n ) = ( 1 ... 1 ) )
200 sneq 
 |-  ( n = 1 -> { n } = { 1 } )
201 198 199 200 3eqtr4a 
 |-  ( n = 1 -> ( 1 ... n ) = { n } )
202 201 raleqdv 
 |-  ( n = 1 -> ( A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) <-> A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) )
203 202 biimprd 
 |-  ( n = 1 -> ( A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) )
204 195 203 syl6 
 |-  ( ( n - 1 ) = 0 -> ( n e. ( 1 ... N ) -> ( A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) ) )
205 ralun 
 |-  ( ( A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) /\ A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) -> A. b e. ( ( 1 ... ( n - 1 ) ) u. { n } ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) )
206 npcan1 
 |-  ( n e. CC -> ( ( n - 1 ) + 1 ) = n )
207 192 206 syl 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) + 1 ) = n )
208 elfzuz 
 |-  ( n e. ( 1 ... N ) -> n e. ( ZZ>= ` 1 ) )
209 207 208 eqeltrd 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
210 peano2zm 
 |-  ( n e. ZZ -> ( n - 1 ) e. ZZ )
211 uzid 
 |-  ( ( n - 1 ) e. ZZ -> ( n - 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
212 peano2uz 
 |-  ( ( n - 1 ) e. ( ZZ>= ` ( n - 1 ) ) -> ( ( n - 1 ) + 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
213 42 210 211 212 4syl 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) + 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
214 207 213 eqeltrrd 
 |-  ( n e. ( 1 ... N ) -> n e. ( ZZ>= ` ( n - 1 ) ) )
215 fzsplit2 
 |-  ( ( ( ( n - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` ( n - 1 ) ) ) -> ( 1 ... n ) = ( ( 1 ... ( n - 1 ) ) u. ( ( ( n - 1 ) + 1 ) ... n ) ) )
216 209 214 215 syl2anc 
 |-  ( n e. ( 1 ... N ) -> ( 1 ... n ) = ( ( 1 ... ( n - 1 ) ) u. ( ( ( n - 1 ) + 1 ) ... n ) ) )
217 207 oveq1d 
 |-  ( n e. ( 1 ... N ) -> ( ( ( n - 1 ) + 1 ) ... n ) = ( n ... n ) )
218 fzsn 
 |-  ( n e. ZZ -> ( n ... n ) = { n } )
219 42 218 syl 
 |-  ( n e. ( 1 ... N ) -> ( n ... n ) = { n } )
220 217 219 eqtrd 
 |-  ( n e. ( 1 ... N ) -> ( ( ( n - 1 ) + 1 ) ... n ) = { n } )
221 220 uneq2d 
 |-  ( n e. ( 1 ... N ) -> ( ( 1 ... ( n - 1 ) ) u. ( ( ( n - 1 ) + 1 ) ... n ) ) = ( ( 1 ... ( n - 1 ) ) u. { n } ) )
222 216 221 eqtrd 
 |-  ( n e. ( 1 ... N ) -> ( 1 ... n ) = ( ( 1 ... ( n - 1 ) ) u. { n } ) )
223 222 raleqdv 
 |-  ( n e. ( 1 ... N ) -> ( A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) <-> A. b e. ( ( 1 ... ( n - 1 ) ) u. { n } ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) )
224 205 223 imbitrrid 
 |-  ( n e. ( 1 ... N ) -> ( ( A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) /\ A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) -> A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) )
225 224 expd 
 |-  ( n e. ( 1 ... N ) -> ( A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> ( A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) ) )
226 225 com12 
 |-  ( A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> ( n e. ( 1 ... N ) -> ( A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) ) )
227 226 adantl 
 |-  ( ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) -> ( n e. ( 1 ... N ) -> ( A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) ) )
228 204 227 jaoi 
 |-  ( ( ( n - 1 ) = 0 \/ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) ) -> ( n e. ( 1 ... N ) -> ( A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) -> A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) ) )
229 228 imdistand 
 |-  ( ( ( n - 1 ) = 0 \/ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) ) -> ( ( n e. ( 1 ... N ) /\ A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) -> ( n e. ( 1 ... N ) /\ A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) ) )
230 229 com12 
 |-  ( ( n e. ( 1 ... N ) /\ A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) -> ( ( ( n - 1 ) = 0 \/ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) ) -> ( n e. ( 1 ... N ) /\ A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) ) )
231 elun 
 |-  ( ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) <-> ( ( n - 1 ) e. { 0 } \/ ( n - 1 ) e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) )
232 ovex 
 |-  ( n - 1 ) e. _V
233 232 elsn 
 |-  ( ( n - 1 ) e. { 0 } <-> ( n - 1 ) = 0 )
234 oveq2 
 |-  ( a = ( n - 1 ) -> ( 1 ... a ) = ( 1 ... ( n - 1 ) ) )
235 234 raleqdv 
 |-  ( a = ( n - 1 ) -> ( A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) <-> A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) )
236 235 elrab 
 |-  ( ( n - 1 ) e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } <-> ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) )
237 233 236 orbi12i 
 |-  ( ( ( n - 1 ) e. { 0 } \/ ( n - 1 ) e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) <-> ( ( n - 1 ) = 0 \/ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) ) )
238 231 237 bitri 
 |-  ( ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) <-> ( ( n - 1 ) = 0 \/ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) ) )
239 oveq2 
 |-  ( a = n -> ( 1 ... a ) = ( 1 ... n ) )
240 239 raleqdv 
 |-  ( a = n -> ( A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) <-> A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) )
241 240 elrab 
 |-  ( n e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } <-> ( n e. ( 1 ... N ) /\ A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) )
242 230 238 241 3imtr4g 
 |-  ( ( n e. ( 1 ... N ) /\ A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) -> ( ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) -> n e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) )
243 elun2 
 |-  ( n e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } -> n e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) )
244 242 243 syl6 
 |-  ( ( n e. ( 1 ... N ) /\ A. b e. { n } ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) ) -> ( ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) -> n e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) ) )
245 101 191 244 syl2anc 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> ( ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) -> n e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) ) )
246 fimaxre2 
 |-  ( ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) C_ RR /\ ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) e. Fin ) -> E. i e. RR A. j e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) j <_ i )
247 47 33 246 mp2an 
 |-  E. i e. RR A. j e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) j <_ i
248 47 38 247 3pm3.2i 
 |-  ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) C_ RR /\ ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) =/= (/) /\ E. i e. RR A. j e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) j <_ i )
249 248 suprubii 
 |-  ( n e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) -> n <_ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) )
250 245 249 syl6 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> ( ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) -> n <_ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) ) )
251 ltm1 
 |-  ( n e. RR -> ( n - 1 ) < n )
252 peano2rem 
 |-  ( n e. RR -> ( n - 1 ) e. RR )
253 47 50 sselii 
 |-  sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) e. RR
254 ltletr 
 |-  ( ( ( n - 1 ) e. RR /\ n e. RR /\ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) e. RR ) -> ( ( ( n - 1 ) < n /\ n <_ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) ) -> ( n - 1 ) < sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) ) )
255 253 254 mp3an3 
 |-  ( ( ( n - 1 ) e. RR /\ n e. RR ) -> ( ( ( n - 1 ) < n /\ n <_ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) ) -> ( n - 1 ) < sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) ) )
256 252 255 mpancom 
 |-  ( n e. RR -> ( ( ( n - 1 ) < n /\ n <_ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) ) -> ( n - 1 ) < sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) ) )
257 251 256 mpand 
 |-  ( n e. RR -> ( n <_ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) -> ( n - 1 ) < sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) ) )
258 100 250 257 sylsyld 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> ( ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) -> ( n - 1 ) < sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) ) )
259 253 ltnri 
 |-  -. sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) < sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < )
260 breq1 
 |-  ( sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) = ( n - 1 ) -> ( sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) < sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) <-> ( n - 1 ) < sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) ) )
261 259 260 mtbii 
 |-  ( sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) = ( n - 1 ) -> -. ( n - 1 ) < sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) )
262 261 necon2ai 
 |-  ( ( n - 1 ) < sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) =/= ( n - 1 ) )
263 258 262 syl6 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> ( ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) =/= ( n - 1 ) ) )
264 eleq1 
 |-  ( sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) = ( n - 1 ) -> ( sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) <-> ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) ) )
265 50 264 mpbii 
 |-  ( sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) = ( n - 1 ) -> ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) )
266 265 necon3bi 
 |-  ( -. ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) =/= ( n - 1 ) )
267 263 266 pm2.61d1 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ p : ( 1 ... N ) --> ( 0 ... k ) /\ ( p ` n ) = k ) ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( p oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( p ` b ) =/= 0 ) } ) , RR , < ) =/= ( n - 1 ) )
268 7 17 53 97 267 179 poimirlem28 
 |-  ( ( ph /\ k e. NN ) -> E. s e. ( ( ( 0 ..^ k ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) )
269 nn0ex 
 |-  NN0 e. _V
270 fzo0ssnn0 
 |-  ( 0 ..^ k ) C_ NN0
271 mapss 
 |-  ( ( NN0 e. _V /\ ( 0 ..^ k ) C_ NN0 ) -> ( ( 0 ..^ k ) ^m ( 1 ... N ) ) C_ ( NN0 ^m ( 1 ... N ) ) )
272 269 270 271 mp2an 
 |-  ( ( 0 ..^ k ) ^m ( 1 ... N ) ) C_ ( NN0 ^m ( 1 ... N ) )
273 xpss1 
 |-  ( ( ( 0 ..^ k ) ^m ( 1 ... N ) ) C_ ( NN0 ^m ( 1 ... N ) ) -> ( ( ( 0 ..^ k ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) C_ ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
274 272 273 ax-mp 
 |-  ( ( ( 0 ..^ k ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) C_ ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
275 274 sseli 
 |-  ( s e. ( ( ( 0 ..^ k ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
276 xp1st 
 |-  ( s e. ( ( ( 0 ..^ k ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` s ) e. ( ( 0 ..^ k ) ^m ( 1 ... N ) ) )
277 elmapi 
 |-  ( ( 1st ` s ) e. ( ( 0 ..^ k ) ^m ( 1 ... N ) ) -> ( 1st ` s ) : ( 1 ... N ) --> ( 0 ..^ k ) )
278 frn 
 |-  ( ( 1st ` s ) : ( 1 ... N ) --> ( 0 ..^ k ) -> ran ( 1st ` s ) C_ ( 0 ..^ k ) )
279 276 277 278 3syl 
 |-  ( s e. ( ( ( 0 ..^ k ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ran ( 1st ` s ) C_ ( 0 ..^ k ) )
280 275 279 jca 
 |-  ( s e. ( ( ( 0 ..^ k ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ ran ( 1st ` s ) C_ ( 0 ..^ k ) ) )
281 280 anim1i 
 |-  ( ( s e. ( ( ( 0 ..^ k ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) -> ( ( s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ ran ( 1st ` s ) C_ ( 0 ..^ k ) ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
282 anass 
 |-  ( ( ( s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ ran ( 1st ` s ) C_ ( 0 ..^ k ) ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) <-> ( s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) )
283 281 282 sylib 
 |-  ( ( s e. ( ( ( 0 ..^ k ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) -> ( s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) )
284 283 reximi2 
 |-  ( E. s e. ( ( ( 0 ..^ k ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) -> E. s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
285 268 284 syl 
 |-  ( ( ph /\ k e. NN ) -> E. s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
286 285 ralrimiva 
 |-  ( ph -> A. k e. NN E. s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
287 nnex 
 |-  NN e. _V
288 144 269 ixpconst 
 |-  X_ n e. ( 1 ... N ) NN0 = ( NN0 ^m ( 1 ... N ) )
289 omelon 
 |-  _om e. On
290 nn0ennn 
 |-  NN0 ~~ NN
291 nnenom 
 |-  NN ~~ _om
292 290 291 entr2i 
 |-  _om ~~ NN0
293 isnumi 
 |-  ( ( _om e. On /\ _om ~~ NN0 ) -> NN0 e. dom card )
294 289 292 293 mp2an 
 |-  NN0 e. dom card
295 294 rgenw 
 |-  A. n e. ( 1 ... N ) NN0 e. dom card
296 finixpnum 
 |-  ( ( ( 1 ... N ) e. Fin /\ A. n e. ( 1 ... N ) NN0 e. dom card ) -> X_ n e. ( 1 ... N ) NN0 e. dom card )
297 29 295 296 mp2an 
 |-  X_ n e. ( 1 ... N ) NN0 e. dom card
298 288 297 eqeltrri 
 |-  ( NN0 ^m ( 1 ... N ) ) e. dom card
299 144 144 mapval 
 |-  ( ( 1 ... N ) ^m ( 1 ... N ) ) = { f | f : ( 1 ... N ) --> ( 1 ... N ) }
300 mapfi 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( 1 ... N ) ^m ( 1 ... N ) ) e. Fin )
301 29 29 300 mp2an 
 |-  ( ( 1 ... N ) ^m ( 1 ... N ) ) e. Fin
302 299 301 eqeltrri 
 |-  { f | f : ( 1 ... N ) --> ( 1 ... N ) } e. Fin
303 f1of 
 |-  ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> f : ( 1 ... N ) --> ( 1 ... N ) )
304 303 ss2abi 
 |-  { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } C_ { f | f : ( 1 ... N ) --> ( 1 ... N ) }
305 ssfi 
 |-  ( ( { f | f : ( 1 ... N ) --> ( 1 ... N ) } e. Fin /\ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } C_ { f | f : ( 1 ... N ) --> ( 1 ... N ) } ) -> { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin )
306 302 304 305 mp2an 
 |-  { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin
307 finnum 
 |-  ( { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. Fin -> { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. dom card )
308 306 307 ax-mp 
 |-  { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. dom card
309 xpnum 
 |-  ( ( ( NN0 ^m ( 1 ... N ) ) e. dom card /\ { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } e. dom card ) -> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) e. dom card )
310 298 308 309 mp2an 
 |-  ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) e. dom card
311 ssrab2 
 |-  { s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) } C_ ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
312 311 rgenw 
 |-  A. k e. NN { s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) } C_ ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
313 ss2iun 
 |-  ( A. k e. NN { s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) } C_ ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> U_ k e. NN { s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) } C_ U_ k e. NN ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
314 312 313 ax-mp 
 |-  U_ k e. NN { s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) } C_ U_ k e. NN ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
315 1nn 
 |-  1 e. NN
316 ne0i 
 |-  ( 1 e. NN -> NN =/= (/) )
317 iunconst 
 |-  ( NN =/= (/) -> U_ k e. NN ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) = ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
318 315 316 317 mp2b 
 |-  U_ k e. NN ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) = ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
319 314 318 sseqtri 
 |-  U_ k e. NN { s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) } C_ ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
320 ssnum 
 |-  ( ( ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) e. dom card /\ U_ k e. NN { s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) } C_ ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) -> U_ k e. NN { s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) } e. dom card )
321 310 319 320 mp2an 
 |-  U_ k e. NN { s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) } e. dom card
322 fveq2 
 |-  ( s = ( g ` k ) -> ( 1st ` s ) = ( 1st ` ( g ` k ) ) )
323 322 rneqd 
 |-  ( s = ( g ` k ) -> ran ( 1st ` s ) = ran ( 1st ` ( g ` k ) ) )
324 323 sseq1d 
 |-  ( s = ( g ` k ) -> ( ran ( 1st ` s ) C_ ( 0 ..^ k ) <-> ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) ) )
325 fveq2 
 |-  ( s = ( g ` k ) -> ( 2nd ` s ) = ( 2nd ` ( g ` k ) ) )
326 325 imaeq1d 
 |-  ( s = ( g ` k ) -> ( ( 2nd ` s ) " ( 1 ... j ) ) = ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) )
327 326 xpeq1d 
 |-  ( s = ( g ` k ) -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) )
328 325 imaeq1d 
 |-  ( s = ( g ` k ) -> ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) )
329 328 xpeq1d 
 |-  ( s = ( g ` k ) -> ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
330 327 329 uneq12d 
 |-  ( s = ( g ` k ) -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
331 322 330 oveq12d 
 |-  ( s = ( g ` k ) -> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
332 331 fvoveq1d 
 |-  ( s = ( g ` k ) -> ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) = ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) )
333 332 fveq1d 
 |-  ( s = ( g ` k ) -> ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) = ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) )
334 333 breq2d 
 |-  ( s = ( g ` k ) -> ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) <-> 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) ) )
335 331 fveq1d 
 |-  ( s = ( g ` k ) -> ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) = ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) )
336 335 neeq1d 
 |-  ( s = ( g ` k ) -> ( ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 <-> ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) )
337 334 336 anbi12d 
 |-  ( s = ( g ` k ) -> ( ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) <-> ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) ) )
338 337 ralbidv 
 |-  ( s = ( g ` k ) -> ( A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) <-> A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) ) )
339 338 rabbidv 
 |-  ( s = ( g ` k ) -> { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } = { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } )
340 339 uneq2d 
 |-  ( s = ( g ` k ) -> ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) = ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) )
341 340 supeq1d 
 |-  ( s = ( g ` k ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) )
342 341 eqeq2d 
 |-  ( s = ( g ` k ) -> ( i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) <-> i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
343 342 rexbidv 
 |-  ( s = ( g ` k ) -> ( E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) <-> E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
344 343 ralbidv 
 |-  ( s = ( g ` k ) -> ( A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) <-> A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
345 324 344 anbi12d 
 |-  ( s = ( g ` k ) -> ( ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) <-> ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) )
346 345 ac6num 
 |-  ( ( NN e. _V /\ U_ k e. NN { s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) | ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) } e. dom card /\ A. k e. NN E. s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) -> E. g ( g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) )
347 287 321 346 mp3an12 
 |-  ( A. k e. NN E. s e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( ran ( 1st ` s ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) -> E. g ( g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) )
348 286 347 syl 
 |-  ( ph -> E. g ( g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) )
349 1 ad2antrr 
 |-  ( ( ( ph /\ g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) -> N e. NN )
350 4 ad2antrr 
 |-  ( ( ( ph /\ g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) -> F e. ( ( R |`t I ) Cn R ) )
351 eqid 
 |-  ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` n ) = ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` n )
352 simplr 
 |-  ( ( ( ph /\ g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) -> g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
353 simpl 
 |-  ( ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) -> ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) )
354 353 ralimi 
 |-  ( A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) -> A. k e. NN ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) )
355 354 adantl 
 |-  ( ( ( ph /\ g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) -> A. k e. NN ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) )
356 2fveq3 
 |-  ( k = p -> ( 1st ` ( g ` k ) ) = ( 1st ` ( g ` p ) ) )
357 356 rneqd 
 |-  ( k = p -> ran ( 1st ` ( g ` k ) ) = ran ( 1st ` ( g ` p ) ) )
358 oveq2 
 |-  ( k = p -> ( 0 ..^ k ) = ( 0 ..^ p ) )
359 357 358 sseq12d 
 |-  ( k = p -> ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) <-> ran ( 1st ` ( g ` p ) ) C_ ( 0 ..^ p ) ) )
360 359 rspccva 
 |-  ( ( A. k e. NN ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ p e. NN ) -> ran ( 1st ` ( g ` p ) ) C_ ( 0 ..^ p ) )
361 355 360 sylan 
 |-  ( ( ( ( ph /\ g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) /\ p e. NN ) -> ran ( 1st ` ( g ` p ) ) C_ ( 0 ..^ p ) )
362 simpll 
 |-  ( ( ( ph /\ g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) -> ph )
363 362 5 sylan 
 |-  ( ( ( ( ph /\ g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 0 ) ) -> ( ( F ` z ) ` n ) <_ 0 )
364 eqid 
 |-  ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) )
365 simpr 
 |-  ( ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) -> A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) )
366 365 ralimi 
 |-  ( A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) -> A. k e. NN A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) )
367 366 adantl 
 |-  ( ( ( ph /\ g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) -> A. k e. NN A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) )
368 2fveq3 
 |-  ( k = p -> ( 2nd ` ( g ` k ) ) = ( 2nd ` ( g ` p ) ) )
369 368 imaeq1d 
 |-  ( k = p -> ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) )
370 369 xpeq1d 
 |-  ( k = p -> ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) )
371 368 imaeq1d 
 |-  ( k = p -> ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) )
372 371 xpeq1d 
 |-  ( k = p -> ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
373 370 372 uneq12d 
 |-  ( k = p -> ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
374 356 373 oveq12d 
 |-  ( k = p -> ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
375 sneq 
 |-  ( k = p -> { k } = { p } )
376 375 xpeq2d 
 |-  ( k = p -> ( ( 1 ... N ) X. { k } ) = ( ( 1 ... N ) X. { p } ) )
377 374 376 oveq12d 
 |-  ( k = p -> ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) = ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) )
378 377 fveq2d 
 |-  ( k = p -> ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) = ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) )
379 378 fveq1d 
 |-  ( k = p -> ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) = ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) )
380 379 breq2d 
 |-  ( k = p -> ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) <-> 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) ) )
381 374 fveq1d 
 |-  ( k = p -> ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) = ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) )
382 381 neeq1d 
 |-  ( k = p -> ( ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 <-> ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) )
383 380 382 anbi12d 
 |-  ( k = p -> ( ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) <-> ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) ) )
384 383 ralbidv 
 |-  ( k = p -> ( A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) <-> A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) ) )
385 384 rabbidv 
 |-  ( k = p -> { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } = { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } )
386 385 uneq2d 
 |-  ( k = p -> ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) = ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) )
387 386 supeq1d 
 |-  ( k = p -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) )
388 387 eqeq2d 
 |-  ( k = p -> ( i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) <-> i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
389 388 rexbidv 
 |-  ( k = p -> ( E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) <-> E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
390 eqeq1 
 |-  ( i = q -> ( i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) <-> q = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
391 390 rexbidv 
 |-  ( i = q -> ( E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) <-> E. j e. ( 0 ... N ) q = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
392 oveq2 
 |-  ( j = m -> ( 1 ... j ) = ( 1 ... m ) )
393 392 imaeq2d 
 |-  ( j = m -> ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) )
394 393 xpeq1d 
 |-  ( j = m -> ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) )
395 oveq1 
 |-  ( j = m -> ( j + 1 ) = ( m + 1 ) )
396 395 oveq1d 
 |-  ( j = m -> ( ( j + 1 ) ... N ) = ( ( m + 1 ) ... N ) )
397 396 imaeq2d 
 |-  ( j = m -> ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) )
398 397 xpeq1d 
 |-  ( j = m -> ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) )
399 394 398 uneq12d 
 |-  ( j = m -> ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) )
400 399 oveq2d 
 |-  ( j = m -> ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) )
401 400 fvoveq1d 
 |-  ( j = m -> ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) = ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) )
402 401 fveq1d 
 |-  ( j = m -> ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) = ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) )
403 402 breq2d 
 |-  ( j = m -> ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) <-> 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) ) )
404 400 fveq1d 
 |-  ( j = m -> ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) = ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) )
405 404 neeq1d 
 |-  ( j = m -> ( ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 <-> ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) )
406 403 405 anbi12d 
 |-  ( j = m -> ( ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) <-> ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) ) )
407 406 ralbidv 
 |-  ( j = m -> ( A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) <-> A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) ) )
408 407 rabbidv 
 |-  ( j = m -> { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } = { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } )
409 408 uneq2d 
 |-  ( j = m -> ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) = ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) )
410 409 supeq1d 
 |-  ( j = m -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) )
411 410 eqeq2d 
 |-  ( j = m -> ( q = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) <-> q = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
412 411 cbvrexvw 
 |-  ( E. j e. ( 0 ... N ) q = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) <-> E. m e. ( 0 ... N ) q = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) )
413 391 412 bitrdi 
 |-  ( i = q -> ( E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) <-> E. m e. ( 0 ... N ) q = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
414 389 413 rspc2v 
 |-  ( ( p e. NN /\ q e. ( 0 ... N ) ) -> ( A. k e. NN A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) -> E. m e. ( 0 ... N ) q = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) )
415 367 414 mpan9 
 |-  ( ( ( ( ph /\ g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) /\ ( p e. NN /\ q e. ( 0 ... N ) ) ) -> E. m e. ( 0 ... N ) q = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) )
416 349 2 3 350 363 364 352 361 415 poimirlem31 
 |-  ( ( ( ( ph /\ g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) /\ ( p e. NN /\ n e. ( 1 ... N ) /\ r e. { <_ , `' <_ } ) ) -> E. m e. ( 0 ... N ) 0 r ( ( F ` ( ( ( 1st ` ( g ` p ) ) oF + ( ( ( ( 2nd ` ( g ` p ) ) " ( 1 ... m ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` p ) ) " ( ( m + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { p } ) ) ) ` n ) )
417 349 2 3 350 351 352 361 416 poimirlem30 
 |-  ( ( ( ph /\ g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) -> 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 ) ) )
418 417 anasss 
 |-  ( ( ph /\ ( g : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ A. k e. NN ( ran ( 1st ` ( g ` k ) ) C_ ( 0 ..^ k ) /\ A. i e. ( 0 ... N ) E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( ( ( 1st ` ( g ` k ) ) oF + ( ( ( ( 2nd ` ( g ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( g ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` b ) =/= 0 ) } ) , RR , < ) ) ) ) -> 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 ) ) )
419 348 418 exlimddv 
 |-  ( 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 ) ) )