poimirlem32

	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	syl6ib	\|- ( ( ( 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	mulid1d	\|- ( 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	syl5ibr	\|- ( 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 ) ) )

Metamath Proof Explorer

Theorem poimirlem32

Proof