Theorem poimirlem13 32017

Description: Lemma for poimir 32037- for at most one simplex associated with a shared face is the opposite vertex first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)

Hypotheses

Ref	Expression
poimir.0	|- ( ph -> N e. NN )
poimirlem22.s	|- S = { t e. ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) }
poimirlem22.1	|- ( ph -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )

Assertion

Ref	Expression
poimirlem13	|- ( ph -> E* z e. S ( 2nd ` z ) = 0 )

Distinct variable groups:   f, j, t, y, z   ph, j, y   j, F, y   j, N, y   ph, t   f, K, j, t   f, N, t   ph, z   f, F, t, z   z, K   z, N   S, j, t, y, z

Allowed substitution hints:   ph( f)   S( f)   K( y)

Proof of Theorem poimirlem13

Dummy variables k m n are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimir.0	. . . . . . . . 9 |- ( ph -> N e. NN )
2	1	ad2antrr 740	. . . . . . . 8 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> N e. NN )
3		poimirlem22.s	. . . . . . . 8 |- S = { t e. ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) }
4		poimirlem22.1	. . . . . . . . 9 |- ( ph -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
5	4	ad2antrr 740	. . . . . . . 8 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
6		simplrl 778	. . . . . . . 8 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> z e. S )
7		simprl 772	. . . . . . . 8 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 2nd ` z ) = 0 )
8	2, 3, 5, 6, 7	poimirlem10 32014	. . . . . . 7 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( ( F ` ( N - 1 ) ) oF - ( ( 1 ... N ) X. { 1 } ) ) = ( 1st ` ( 1st ` z ) ) )
9		simplrr 779	. . . . . . . 8 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> k e. S )
10		simprr 774	. . . . . . . 8 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 2nd ` k ) = 0 )
11	2, 3, 5, 9, 10	poimirlem10 32014	. . . . . . 7 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( ( F ` ( N - 1 ) ) oF - ( ( 1 ... N ) X. { 1 } ) ) = ( 1st ` ( 1st ` k ) ) )
12	8, 11	eqtr3d 2507	. . . . . 6 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` k ) ) )
13		elrabi 3181	. . . . . . . . . . . . . 14 |- ( z e. { t e. ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) } -> z e. ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
14	13, 3	eleq2s 2567	. . . . . . . . . . . . 13 |- ( z e. S -> z e. ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
15		xp1st 6842	. . . . . . . . . . . . 13 |- ( z e. ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 1st ` z ) e. ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
16	14, 15	syl 17	. . . . . . . . . . . 12 |- ( z e. S -> ( 1st ` z ) e. ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
17		xp2nd 6843	. . . . . . . . . . . 12 |- ( ( 1st ` z ) e. ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` ( 1st ` z ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
18	16, 17	syl 17	. . . . . . . . . . 11 |- ( z e. S -> ( 2nd ` ( 1st ` z ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
19		fvex 5889	. . . . . . . . . . . 12 |- ( 2nd ` ( 1st ` z ) ) e. _V
20		f1oeq1 5818	. . . . . . . . . . . 12 |- ( f = ( 2nd ` ( 1st ` z ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
21	19, 20	elab 3173	. . . . . . . . . . 11 |- ( ( 2nd ` ( 1st ` z ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
22	18, 21	sylib 201	. . . . . . . . . 10 |- ( z e. S -> ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
23		f1ofn 5829	. . . . . . . . . 10 |- ( ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` z ) ) Fn ( 1 ... N ) )
24	22, 23	syl 17	. . . . . . . . 9 |- ( z e. S -> ( 2nd ` ( 1st ` z ) ) Fn ( 1 ... N ) )
25	24	adantr 472	. . . . . . . 8 |- ( ( z e. S /\ k e. S ) -> ( 2nd ` ( 1st ` z ) ) Fn ( 1 ... N ) )
26	25	ad2antlr 741	. . . . . . 7 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 2nd ` ( 1st ` z ) ) Fn ( 1 ... N ) )
27		elrabi 3181	. . . . . . . . . . . . . 14 |- ( k e. { t e. ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) } -> k e. ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
28	27, 3	eleq2s 2567	. . . . . . . . . . . . 13 |- ( k e. S -> k e. ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
29		xp1st 6842	. . . . . . . . . . . . 13 |- ( k e. ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 1st ` k ) e. ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
30	28, 29	syl 17	. . . . . . . . . . . 12 |- ( k e. S -> ( 1st ` k ) e. ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
31		xp2nd 6843	. . . . . . . . . . . 12 |- ( ( 1st ` k ) e. ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` ( 1st ` k ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
32	30, 31	syl 17	. . . . . . . . . . 11 |- ( k e. S -> ( 2nd ` ( 1st ` k ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
33		fvex 5889	. . . . . . . . . . . 12 |- ( 2nd ` ( 1st ` k ) ) e. _V
34		f1oeq1 5818	. . . . . . . . . . . 12 |- ( f = ( 2nd ` ( 1st ` k ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
35	33, 34	elab 3173	. . . . . . . . . . 11 |- ( ( 2nd ` ( 1st ` k ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
36	32, 35	sylib 201	. . . . . . . . . 10 |- ( k e. S -> ( 2nd ` ( 1st ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
37		f1ofn 5829	. . . . . . . . . 10 |- ( ( 2nd ` ( 1st ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` k ) ) Fn ( 1 ... N ) )
38	36, 37	syl 17	. . . . . . . . 9 |- ( k e. S -> ( 2nd ` ( 1st ` k ) ) Fn ( 1 ... N ) )
39	38	adantl 473	. . . . . . . 8 |- ( ( z e. S /\ k e. S ) -> ( 2nd ` ( 1st ` k ) ) Fn ( 1 ... N ) )
40	39	ad2antlr 741	. . . . . . 7 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 2nd ` ( 1st ` k ) ) Fn ( 1 ... N ) )
41		eleq1 2537	. . . . . . . . . . . . 13 |- ( m = n -> ( m e. ( 1 ... N ) <-> n e. ( 1 ... N ) ) )
42	41	anbi2d 718	. . . . . . . . . . . 12 |- ( m = n -> ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) <-> ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) ) )
43		oveq2 6316	. . . . . . . . . . . . . 14 |- ( m = n -> ( 1 ... m ) = ( 1 ... n ) )
44	43	imaeq2d 5174	. . . . . . . . . . . . 13 |- ( m = n -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) )
45	43	imaeq2d 5174	. . . . . . . . . . . . 13 |- ( m = n -> ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) )
46	44, 45	eqeq12d 2486	. . . . . . . . . . . 12 |- ( m = n -> ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) <-> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) ) )
47	42, 46	imbi12d 327	. . . . . . . . . . 11 |- ( m = n -> ( ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) ) <-> ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) ) ) )
48	1	ad3antrrr 744	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> N e. NN )
49	4	ad3antrrr 744	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
50		simpl 464	. . . . . . . . . . . . . 14 |- ( ( z e. S /\ k e. S ) -> z e. S )
51	50	ad3antlr 745	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> z e. S )
52		simplrl 778	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( 2nd ` z ) = 0 )
53		simpr 468	. . . . . . . . . . . . . 14 |- ( ( z e. S /\ k e. S ) -> k e. S )
54	53	ad3antlr 745	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> k e. S )
55		simplrr 779	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( 2nd ` k ) = 0 )
56		simpr 468	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> m e. ( 1 ... N ) )
57	48, 3, 49, 51, 52, 54, 55, 56	poimirlem11 32015	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) C_ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) )
58	48, 3, 49, 54, 55, 51, 52, 56	poimirlem11 32015	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) C_ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) )
59	57, 58	eqssd 3435	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) )
60	47, 59	chvarv 2120	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) )
61		simpll 768	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ph )
62		elfznn 11854	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( 1 ... N ) -> n e. NN )
63		nnm1nn0 10935	. . . . . . . . . . . . . . . . . . 19 |- ( n e. NN -> ( n - 1 ) e. NN0 )
64	62, 63	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( 1 ... N ) -> ( n - 1 ) e. NN0 )
65	64	adantr 472	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( 1 ... N ) /\ -. n = 1 ) -> ( n - 1 ) e. NN0 )
66	62	nncnd 10647	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. ( 1 ... N ) -> n e. CC )
67		ax-1cn 9615	. . . . . . . . . . . . . . . . . . . 20 |- 1 e. CC
68		subeq0 9920	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. CC /\ 1 e. CC ) -> ( ( n - 1 ) = 0 <-> n = 1 ) )
69	66, 67, 68	sylancl 675	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( 1 ... N ) -> ( ( n - 1 ) = 0 <-> n = 1 ) )
70	69	necon3abid 2679	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( 1 ... N ) -> ( ( n - 1 ) =/= 0 <-> -. n = 1 ) )
71	70	biimpar 493	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( 1 ... N ) /\ -. n = 1 ) -> ( n - 1 ) =/= 0 )
72		elnnne0 10907	. . . . . . . . . . . . . . . . 17 |- ( ( n - 1 ) e. NN <-> ( ( n - 1 ) e. NN0 /\ ( n - 1 ) =/= 0 ) )
73	65, 71, 72	sylanbrc 677	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( 1 ... N ) /\ -. n = 1 ) -> ( n - 1 ) e. NN )
74	73	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( n e. ( 1 ... N ) /\ -. n = 1 ) ) -> ( n - 1 ) e. NN )
75	64	nn0red 10950	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( 1 ... N ) -> ( n - 1 ) e. RR )
76	75	adantl 473	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( n - 1 ) e. RR )
77	62	nnred 10646	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( 1 ... N ) -> n e. RR )
78	77	adantl 473	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. ( 1 ... N ) ) -> n e. RR )
79	1	nnred 10646	. . . . . . . . . . . . . . . . . 18 |- ( ph -> N e. RR )
80	79	adantr 472	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. ( 1 ... N ) ) -> N e. RR )
81	77	lem1d 10562	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( 1 ... N ) -> ( n - 1 ) <_ n )
82	81	adantl 473	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( n - 1 ) <_ n )
83		elfzle2 11829	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( 1 ... N ) -> n <_ N )
84	83	adantl 473	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. ( 1 ... N ) ) -> n <_ N )
85	76, 78, 80, 82, 84	letrd 9809	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( n - 1 ) <_ N )
86	85	adantrr 731	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( n e. ( 1 ... N ) /\ -. n = 1 ) ) -> ( n - 1 ) <_ N )
87	1	nnzd 11062	. . . . . . . . . . . . . . . . 17 |- ( ph -> N e. ZZ )
88		fznn 11889	. . . . . . . . . . . . . . . . 17 |- ( N e. ZZ -> ( ( n - 1 ) e. ( 1 ... N ) <-> ( ( n - 1 ) e. NN /\ ( n - 1 ) <_ N ) ) )
89	87, 88	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( n - 1 ) e. ( 1 ... N ) <-> ( ( n - 1 ) e. NN /\ ( n - 1 ) <_ N ) ) )
90	89	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( n e. ( 1 ... N ) /\ -. n = 1 ) ) -> ( ( n - 1 ) e. ( 1 ... N ) <-> ( ( n - 1 ) e. NN /\ ( n - 1 ) <_ N ) ) )
91	74, 86, 90	mpbir2and 936	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( n e. ( 1 ... N ) /\ -. n = 1 ) ) -> ( n - 1 ) e. ( 1 ... N ) )
92	61, 91	sylan 479	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ ( n e. ( 1 ... N ) /\ -. n = 1 ) ) -> ( n - 1 ) e. ( 1 ... N ) )
93		ovex 6336	. . . . . . . . . . . . . 14 |- ( n - 1 ) e. _V
94		eleq1 2537	. . . . . . . . . . . . . . . 16 |- ( m = ( n - 1 ) -> ( m e. ( 1 ... N ) <-> ( n - 1 ) e. ( 1 ... N ) ) )
95	94	anbi2d 718	. . . . . . . . . . . . . . 15 |- ( m = ( n - 1 ) -> ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) <-> ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ ( n - 1 ) e. ( 1 ... N ) ) ) )
96		oveq2 6316	. . . . . . . . . . . . . . . . 17 |- ( m = ( n - 1 ) -> ( 1 ... m ) = ( 1 ... ( n - 1 ) ) )
97	96	imaeq2d 5174	. . . . . . . . . . . . . . . 16 |- ( m = ( n - 1 ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) )
98	96	imaeq2d 5174	. . . . . . . . . . . . . . . 16 |- ( m = ( n - 1 ) -> ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) )
99	97, 98	eqeq12d 2486	. . . . . . . . . . . . . . 15 |- ( m = ( n - 1 ) -> ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) <-> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) )
100	95, 99	imbi12d 327	. . . . . . . . . . . . . 14 |- ( m = ( n - 1 ) -> ( ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ m e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... m ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... m ) ) ) <-> ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ ( n - 1 ) e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) ) )
101	93, 100, 59	vtocl 3086	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ ( n - 1 ) e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) )
102	92, 101	syldan 478	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ ( n e. ( 1 ... N ) /\ -. n = 1 ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) )
103	102	expr 626	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( -. n = 1 -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) )
104		ima0 5189	. . . . . . . . . . . . 13 |- ( ( 2nd ` ( 1st ` z ) ) " (/) ) = (/)
105		ima0 5189	. . . . . . . . . . . . 13 |- ( ( 2nd ` ( 1st ` k ) ) " (/) ) = (/)
106	104, 105	eqtr4i 2496	. . . . . . . . . . . 12 |- ( ( 2nd ` ( 1st ` z ) ) " (/) ) = ( ( 2nd ` ( 1st ` k ) ) " (/) )
107		oveq1 6315	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
108		1m1e0 10700	. . . . . . . . . . . . . . . 16 |- ( 1 - 1 ) = 0
109	107, 108	syl6eq 2521	. . . . . . . . . . . . . . 15 |- ( n = 1 -> ( n - 1 ) = 0 )
110	109	oveq2d 6324	. . . . . . . . . . . . . 14 |- ( n = 1 -> ( 1 ... ( n - 1 ) ) = ( 1 ... 0 ) )
111		fz10 11846	. . . . . . . . . . . . . 14 |- ( 1 ... 0 ) = (/)
112	110, 111	syl6eq 2521	. . . . . . . . . . . . 13 |- ( n = 1 -> ( 1 ... ( n - 1 ) ) = (/) )
113	112	imaeq2d 5174	. . . . . . . . . . . 12 |- ( n = 1 -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` z ) ) " (/) ) )
114	112	imaeq2d 5174	. . . . . . . . . . . 12 |- ( n = 1 -> ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " (/) ) )
115	106, 113, 114	3eqtr4a 2531	. . . . . . . . . . 11 |- ( n = 1 -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) )
116	103, 115	pm2.61d2 165	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) )
117	60, 116	difeq12d 3541	. . . . . . . . 9 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) )
118		fnsnfv 5940	. . . . . . . . . . . 12 |- ( ( ( 2nd ` ( 1st ` z ) ) Fn ( 1 ... N ) /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = ( ( 2nd ` ( 1st ` z ) ) " { n } ) )
119	24, 118	sylan 479	. . . . . . . . . . 11 |- ( ( z e. S /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = ( ( 2nd ` ( 1st ` z ) ) " { n } ) )
120	62	adantl 473	. . . . . . . . . . . . 13 |- ( ( z e. S /\ n e. ( 1 ... N ) ) -> n e. NN )
121		uncom 3569	. . . . . . . . . . . . . . . 16 |- ( ( 1 ... ( n - 1 ) ) u. { n } ) = ( { n } u. ( 1 ... ( n - 1 ) ) )
122	121	difeq1i 3536	. . . . . . . . . . . . . . 15 |- ( ( ( 1 ... ( n - 1 ) ) u. { n } ) \ ( 1 ... ( n - 1 ) ) ) = ( ( { n } u. ( 1 ... ( n - 1 ) ) ) \ ( 1 ... ( n - 1 ) ) )
123		difun2 3838	. . . . . . . . . . . . . . 15 |- ( ( { n } u. ( 1 ... ( n - 1 ) ) ) \ ( 1 ... ( n - 1 ) ) ) = ( { n } \ ( 1 ... ( n - 1 ) ) )
124	122, 123	eqtri 2493	. . . . . . . . . . . . . 14 |- ( ( ( 1 ... ( n - 1 ) ) u. { n } ) \ ( 1 ... ( n - 1 ) ) ) = ( { n } \ ( 1 ... ( n - 1 ) ) )
125		nncn 10639	. . . . . . . . . . . . . . . . . . 19 |- ( n e. NN -> n e. CC )
126		npcan1 10065	. . . . . . . . . . . . . . . . . . 19 |- ( n e. CC -> ( ( n - 1 ) + 1 ) = n )
127	125, 126	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN -> ( ( n - 1 ) + 1 ) = n )
128		elnnuz 11219	. . . . . . . . . . . . . . . . . . 19 |- ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
129	128	biimpi 199	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN -> n e. ( ZZ>= ` 1 ) )
130	127, 129	eqeltrd 2549	. . . . . . . . . . . . . . . . 17 |- ( n e. NN -> ( ( n - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
131	63	nn0zd 11061	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. NN -> ( n - 1 ) e. ZZ )
132		uzid 11197	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n - 1 ) e. ZZ -> ( n - 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
133	131, 132	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( n e. NN -> ( n - 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
134		peano2uz 11235	. . . . . . . . . . . . . . . . . . 19 |- ( ( n - 1 ) e. ( ZZ>= ` ( n - 1 ) ) -> ( ( n - 1 ) + 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
135	133, 134	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN -> ( ( n - 1 ) + 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
136	127, 135	eqeltrrd 2550	. . . . . . . . . . . . . . . . 17 |- ( n e. NN -> n e. ( ZZ>= ` ( n - 1 ) ) )
137		fzsplit2 11850	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( n - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` ( n - 1 ) ) ) -> ( 1 ... n ) = ( ( 1 ... ( n - 1 ) ) u. ( ( ( n - 1 ) + 1 ) ... n ) ) )
138	130, 136, 137	syl2anc 673	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> ( 1 ... n ) = ( ( 1 ... ( n - 1 ) ) u. ( ( ( n - 1 ) + 1 ) ... n ) ) )
139	127	oveq1d 6323	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN -> ( ( ( n - 1 ) + 1 ) ... n ) = ( n ... n ) )
140		nnz 10983	. . . . . . . . . . . . . . . . . . 19 |- ( n e. NN -> n e. ZZ )
141		fzsn 11866	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ZZ -> ( n ... n ) = { n } )
142	140, 141	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN -> ( n ... n ) = { n } )
143	139, 142	eqtrd 2505	. . . . . . . . . . . . . . . . 17 |- ( n e. NN -> ( ( ( n - 1 ) + 1 ) ... n ) = { n } )
144	143	uneq2d 3579	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> ( ( 1 ... ( n - 1 ) ) u. ( ( ( n - 1 ) + 1 ) ... n ) ) = ( ( 1 ... ( n - 1 ) ) u. { n } ) )
145	138, 144	eqtrd 2505	. . . . . . . . . . . . . . 15 |- ( n e. NN -> ( 1 ... n ) = ( ( 1 ... ( n - 1 ) ) u. { n } ) )
146	145	difeq1d 3539	. . . . . . . . . . . . . 14 |- ( n e. NN -> ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) = ( ( ( 1 ... ( n - 1 ) ) u. { n } ) \ ( 1 ... ( n - 1 ) ) ) )
147		nnre 10638	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> n e. RR )
148		ltm1 10467	. . . . . . . . . . . . . . . . . 18 |- ( n e. RR -> ( n - 1 ) < n )
149		peano2rem 9961	. . . . . . . . . . . . . . . . . . 19 |- ( n e. RR -> ( n - 1 ) e. RR )
150		ltnle 9731	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( n - 1 ) e. RR /\ n e. RR ) -> ( ( n - 1 ) < n <-> -. n <_ ( n - 1 ) ) )
151	149, 150	mpancom 682	. . . . . . . . . . . . . . . . . 18 |- ( n e. RR -> ( ( n - 1 ) < n <-> -. n <_ ( n - 1 ) ) )
152	148, 151	mpbid 215	. . . . . . . . . . . . . . . . 17 |- ( n e. RR -> -. n <_ ( n - 1 ) )
153		elfzle2 11829	. . . . . . . . . . . . . . . . 17 |- ( n e. ( 1 ... ( n - 1 ) ) -> n <_ ( n - 1 ) )
154	152, 153	nsyl 125	. . . . . . . . . . . . . . . 16 |- ( n e. RR -> -. n e. ( 1 ... ( n - 1 ) ) )
155	147, 154	syl 17	. . . . . . . . . . . . . . 15 |- ( n e. NN -> -. n e. ( 1 ... ( n - 1 ) ) )
156		incom 3616	. . . . . . . . . . . . . . . . 17 |- ( ( 1 ... ( n - 1 ) ) i^i { n } ) = ( { n } i^i ( 1 ... ( n - 1 ) ) )
157	156	eqeq1i 2476	. . . . . . . . . . . . . . . 16 |- ( ( ( 1 ... ( n - 1 ) ) i^i { n } ) = (/) <-> ( { n } i^i ( 1 ... ( n - 1 ) ) ) = (/) )
158		disjsn 4023	. . . . . . . . . . . . . . . 16 |- ( ( ( 1 ... ( n - 1 ) ) i^i { n } ) = (/) <-> -. n e. ( 1 ... ( n - 1 ) ) )
159		disj3 3813	. . . . . . . . . . . . . . . 16 |- ( ( { n } i^i ( 1 ... ( n - 1 ) ) ) = (/) <-> { n } = ( { n } \ ( 1 ... ( n - 1 ) ) ) )
160	157, 158, 159	3bitr3i 283	. . . . . . . . . . . . . . 15 |- ( -. n e. ( 1 ... ( n - 1 ) ) <-> { n } = ( { n } \ ( 1 ... ( n - 1 ) ) ) )
161	155, 160	sylib 201	. . . . . . . . . . . . . 14 |- ( n e. NN -> { n } = ( { n } \ ( 1 ... ( n - 1 ) ) ) )
162	124, 146, 161	3eqtr4a 2531	. . . . . . . . . . . . 13 |- ( n e. NN -> ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) = { n } )
163	120, 162	syl 17	. . . . . . . . . . . 12 |- ( ( z e. S /\ n e. ( 1 ... N ) ) -> ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) = { n } )
164	163	imaeq2d 5174	. . . . . . . . . . 11 |- ( ( z e. S /\ n e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) ) = ( ( 2nd ` ( 1st ` z ) ) " { n } ) )
165		dff1o3 5834	. . . . . . . . . . . . . . 15 |- ( ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( 2nd ` ( 1st ` z ) ) ) )
166	165	simprbi 471	. . . . . . . . . . . . . 14 |- ( ( 2nd ` ( 1st ` z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' ( 2nd ` ( 1st ` z ) ) )
167	22, 166	syl 17	. . . . . . . . . . . . 13 |- ( z e. S -> Fun `' ( 2nd ` ( 1st ` z ) ) )
168		imadif 5668	. . . . . . . . . . . . 13 |- ( Fun `' ( 2nd ` ( 1st ` z ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) )
169	167, 168	syl 17	. . . . . . . . . . . 12 |- ( z e. S -> ( ( 2nd ` ( 1st ` z ) ) " ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) )
170	169	adantr 472	. . . . . . . . . . 11 |- ( ( z e. S /\ n e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) " ( ( 1 ... n ) \ ( 1 ... ( n - 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) )
171	119, 164, 170	3eqtr2d 2511	. . . . . . . . . 10 |- ( ( z e. S /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) )
172	6, 171	sylan 479	. . . . . . . . 9 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) )
173		eleq1 2537	. . . . . . . . . . . . 13 |- ( z = k -> ( z e. S <-> k e. S ) )
174	173	anbi1d 719	. . . . . . . . . . . 12 |- ( z = k -> ( ( z e. S /\ n e. ( 1 ... N ) ) <-> ( k e. S /\ n e. ( 1 ... N ) ) ) )
175		fveq2 5879	. . . . . . . . . . . . . . . 16 |- ( z = k -> ( 1st ` z ) = ( 1st ` k ) )
176	175	fveq2d 5883	. . . . . . . . . . . . . . 15 |- ( z = k -> ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` k ) ) )
177	176	fveq1d 5881	. . . . . . . . . . . . . 14 |- ( z = k -> ( ( 2nd ` ( 1st ` z ) ) ` n ) = ( ( 2nd ` ( 1st ` k ) ) ` n ) )
178	177	sneqd 3971	. . . . . . . . . . . . 13 |- ( z = k -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = { ( ( 2nd ` ( 1st ` k ) ) ` n ) } )
179	176	imaeq1d 5173	. . . . . . . . . . . . . 14 |- ( z = k -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) )
180	176	imaeq1d 5173	. . . . . . . . . . . . . 14 |- ( z = k -> ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) = ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) )
181	179, 180	difeq12d 3541	. . . . . . . . . . . . 13 |- ( z = k -> ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) )
182	178, 181	eqeq12d 2486	. . . . . . . . . . . 12 |- ( z = k -> ( { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) <-> { ( ( 2nd ` ( 1st ` k ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) ) )
183	174, 182	imbi12d 327	. . . . . . . . . . 11 |- ( z = k -> ( ( ( z e. S /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` z ) ) " ( 1 ... ( n - 1 ) ) ) ) ) <-> ( ( k e. S /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` k ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) ) ) )
184	183, 171	chvarv 2120	. . . . . . . . . 10 |- ( ( k e. S /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` k ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) )
185	9, 184	sylan 479	. . . . . . . . 9 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` k ) ) ` n ) } = ( ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... n ) ) \ ( ( 2nd ` ( 1st ` k ) ) " ( 1 ... ( n - 1 ) ) ) ) )
186	117, 172, 185	3eqtr4d 2515	. . . . . . . 8 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = { ( ( 2nd ` ( 1st ` k ) ) ` n ) } )
187		fvex 5889	. . . . . . . . 9 |- ( ( 2nd ` ( 1st ` z ) ) ` n ) e. _V
188	187	sneqr 4131	. . . . . . . 8 |- ( { ( ( 2nd ` ( 1st ` z ) ) ` n ) } = { ( ( 2nd ` ( 1st ` k ) ) ` n ) } -> ( ( 2nd ` ( 1st ` z ) ) ` n ) = ( ( 2nd ` ( 1st ` k ) ) ` n ) )
189	186, 188	syl 17	. . . . . . 7 |- ( ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` z ) ) ` n ) = ( ( 2nd ` ( 1st ` k ) ) ` n ) )
190	26, 40, 189	eqfnfvd 5994	. . . . . 6 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` k ) ) )
191		xpopth 6851	. . . . . . . 8 |- ( ( ( 1st ` z ) e. ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ ( 1st ` k ) e. ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ) -> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` k ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` k ) ) ) <-> ( 1st ` z ) = ( 1st ` k ) ) )
192	16, 30, 191	syl2an 485	. . . . . . 7 |- ( ( z e. S /\ k e. S ) -> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` k ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` k ) ) ) <-> ( 1st ` z ) = ( 1st ` k ) ) )
193	192	ad2antlr 741	. . . . . 6 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( ( ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` k ) ) /\ ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` k ) ) ) <-> ( 1st ` z ) = ( 1st ` k ) ) )
194	12, 190, 193	mpbi2and 935	. . . . 5 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 1st ` z ) = ( 1st ` k ) )
195		eqtr3 2492	. . . . . 6 |- ( ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) -> ( 2nd ` z ) = ( 2nd ` k ) )
196	195	adantl 473	. . . . 5 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( 2nd ` z ) = ( 2nd ` k ) )
197		xpopth 6851	. . . . . . 7 |- ( ( z e. ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ k e. ( ( ( ( 0..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) ) -> ( ( ( 1st ` z ) = ( 1st ` k ) /\ ( 2nd ` z ) = ( 2nd ` k ) ) <-> z = k ) )
198	14, 28, 197	syl2an 485	. . . . . 6 |- ( ( z e. S /\ k e. S ) -> ( ( ( 1st ` z ) = ( 1st ` k ) /\ ( 2nd ` z ) = ( 2nd ` k ) ) <-> z = k ) )
199	198	ad2antlr 741	. . . . 5 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> ( ( ( 1st ` z ) = ( 1st ` k ) /\ ( 2nd ` z ) = ( 2nd ` k ) ) <-> z = k ) )
200	194, 196, 199	mpbi2and 935	. . . 4 |- ( ( ( ph /\ ( z e. S /\ k e. S ) ) /\ ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) ) -> z = k )
201	200	ex 441	. . 3 |- ( ( ph /\ ( z e. S /\ k e. S ) ) -> ( ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) -> z = k ) )
202	201	ralrimivva 2814	. 2 |- ( ph -> A. z e. S A. k e. S ( ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) -> z = k ) )
203		fveq2 5879	. . . 4 |- ( z = k -> ( 2nd ` z ) = ( 2nd ` k ) )
204	203	eqeq1d 2473	. . 3 |- ( z = k -> ( ( 2nd ` z ) = 0 <-> ( 2nd ` k ) = 0 ) )
205	204	rmo4 3219	. 2 |- ( E* z e. S ( 2nd ` z ) = 0 <-> A. z e. S A. k e. S ( ( ( 2nd ` z ) = 0 /\ ( 2nd ` k ) = 0 ) -> z = k ) )
206	202, 205	sylibr 217	1 |- ( ph -> E* z e. S ( 2nd ` z ) = 0 )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 376   = wceq 1452   e. wcel 1904   {cab 2457   =/= wne 2641   A.wral 2756   E*wrmo 2759   {crab 2760   [_csb 3349   \ cdif 3387   u. cun 3388   i^i cin 3389   (/)c0 3722   ifcif 3872   {csn 3959   class class class wbr 4395   |-> cmpt 4454   X. cxp 4837   `'ccnv 4838   "cima 4842   Fun wfun 5583   Fn wfn 5584   -->wf 5585   -onto->wfo 5587   -1-1-onto->wf1o 5588   ` cfv 5589  (class class class)co 6308   oFcof 6548   1stc1st 6810   2ndc2nd 6811   ^m cmap 7490   CCcc 9555   RRcr 9556   0cc0 9557   1c1 9558   + caddc 9560   < clt 9693   <_ cle 9694   - cmin 9880   NNcn 10631   NN0cn0 10893   ZZcz 10961   ZZ>=cuz 11182   ...cfz 11810  ..^cfzo 11942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-er 7381  df-map 7492  df-en 7588  df-dom 7589  df-sdom 7590  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-n0 10894  df-z 10962  df-uz 11183  df-fz 11811  df-fzo 11943

This theorem is referenced by:  poimirlem18  32022  poimirlem21  32025