Theorem subfacp1lem5 31166

Description: Lemma for subfacp1 31168. In subfacp1lem6 31167 we cut up the set of all derangements on 1 ... ( N + 1 ) first according to the value at 1, and then by whether or not ( f ` ( f ` 1 ) ) = 1. In this lemma, we show that the subset of all N + 1 derangements with ( f ` ( f ` 1 ) ) =/= 1 for fixed M = ( f ` 1 ) is in bijection with derangements of 2 ... ( N + 1 ), because pre-composing with the function F swaps 1 and M and turns the function into a bijection with ( f ` 1 ) = 1 and ( f ` x ) =/= x for all other x, so dropping the point at 1 yields a derangement on the N remaining points. (Contributed by Mario Carneiro, 23-Jan-2015.)

Hypotheses

Ref	Expression
derang.d	|- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
subfac.n	|- S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
subfacp1lem.a	|- A = { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) }
subfacp1lem1.n	|- ( ph -> N e. NN )
subfacp1lem1.m	|- ( ph -> M e. ( 2 ... ( N + 1 ) ) )
subfacp1lem1.x	|- M e. _V
subfacp1lem1.k	|- K = ( ( 2 ... ( N + 1 ) ) \ { M } )
subfacp1lem5.b	|- B = { g e. A | ( ( g ` 1 ) = M /\ ( g ` M ) =/= 1 ) }
subfacp1lem5.f	|- F = ( ( _I |` K ) u. { <. 1 , M >. , <. M , 1 >. } )
subfacp1lem5.c	|- C = { f | ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) }

Assertion

Ref	Expression
subfacp1lem5	|- ( ph -> ( # ` B ) = ( S ` N ) )

Distinct variable groups:   f, g, n, x, y, A   f, F, g, x, y   f, N, g, n, x, y   B, f, g, x, y   x, C, y   ph, x, y   D, n   f, K, n, x, y   f, M, g, x, y   S, n, x, y

Allowed substitution hints:   ph( f, g, n)   B( n)   C( f, g, n)   D( x, y, f, g)   S( f, g)   F( n)   K( g)   M( n)

Proof of Theorem subfacp1lem5

Dummy variables b c are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		subfacp1lem.a	. . . . . . . 8 |- A = { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) }
2		fzfi 12771	. . . . . . . . 9 |- ( 1 ... ( N + 1 ) ) e. Fin
3		deranglem 31148	. . . . . . . . 9 |- ( ( 1 ... ( N + 1 ) ) e. Fin -> { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) } e. Fin )
4	2, 3	ax-mp 5	. . . . . . . 8 |- { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) } e. Fin
5	1, 4	eqeltri 2697	. . . . . . 7 |- A e. Fin
6		subfacp1lem5.b	. . . . . . . 8 |- B = { g e. A | ( ( g ` 1 ) = M /\ ( g ` M ) =/= 1 ) }
7		ssrab2 3687	. . . . . . . 8 |- { g e. A | ( ( g ` 1 ) = M /\ ( g ` M ) =/= 1 ) } C_ A
8	6, 7	eqsstri 3635	. . . . . . 7 |- B C_ A
9		ssfi 8180	. . . . . . 7 |- ( ( A e. Fin /\ B C_ A ) -> B e. Fin )
10	5, 8, 9	mp2an 708	. . . . . 6 |- B e. Fin
11	10	elexi 3213	. . . . 5 |- B e. _V
12	11	a1i 11	. . . 4 |- ( ph -> B e. _V )
13		subfacp1lem5.c	. . . . . . 7 |- C = { f | ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) }
14		fzfi 12771	. . . . . . . 8 |- ( 2 ... ( N + 1 ) ) e. Fin
15		deranglem 31148	. . . . . . . 8 |- ( ( 2 ... ( N + 1 ) ) e. Fin -> { f | ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) } e. Fin )
16	14, 15	ax-mp 5	. . . . . . 7 |- { f | ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) } e. Fin
17	13, 16	eqeltri 2697	. . . . . 6 |- C e. Fin
18	17	elexi 3213	. . . . 5 |- C e. _V
19	18	a1i 11	. . . 4 |- ( ph -> C e. _V )
20		derang.d	. . . . . . . . . . . . 13 |- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
21		subfac.n	. . . . . . . . . . . . 13 |- S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
22		subfacp1lem1.n	. . . . . . . . . . . . 13 |- ( ph -> N e. NN )
23		subfacp1lem1.m	. . . . . . . . . . . . 13 |- ( ph -> M e. ( 2 ... ( N + 1 ) ) )
24		subfacp1lem1.x	. . . . . . . . . . . . 13 |- M e. _V
25		subfacp1lem1.k	. . . . . . . . . . . . 13 |- K = ( ( 2 ... ( N + 1 ) ) \ { M } )
26		subfacp1lem5.f	. . . . . . . . . . . . 13 |- F = ( ( _I |` K ) u. { <. 1 , M >. , <. M , 1 >. } )
27		f1oi 6174	. . . . . . . . . . . . . 14 |- ( _I |` K ) : K -1-1-onto-> K
28	27	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( _I |` K ) : K -1-1-onto-> K )
29	20, 21, 1, 22, 23, 24, 25, 26, 28	subfacp1lem2a 31162	. . . . . . . . . . . 12 |- ( ph -> ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( F ` 1 ) = M /\ ( F ` M ) = 1 ) )
30	29	simp1d 1073	. . . . . . . . . . 11 |- ( ph -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
31	30	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ b e. B ) -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
32		simpr 477	. . . . . . . . . . . . . 14 |- ( ( ph /\ b e. B ) -> b e. B )
33		fveq1 6190	. . . . . . . . . . . . . . . . 17 |- ( g = b -> ( g ` 1 ) = ( b ` 1 ) )
34	33	eqeq1d 2624	. . . . . . . . . . . . . . . 16 |- ( g = b -> ( ( g ` 1 ) = M <-> ( b ` 1 ) = M ) )
35		fveq1 6190	. . . . . . . . . . . . . . . . 17 |- ( g = b -> ( g ` M ) = ( b ` M ) )
36	35	neeq1d 2853	. . . . . . . . . . . . . . . 16 |- ( g = b -> ( ( g ` M ) =/= 1 <-> ( b ` M ) =/= 1 ) )
37	34, 36	anbi12d 747	. . . . . . . . . . . . . . 15 |- ( g = b -> ( ( ( g ` 1 ) = M /\ ( g ` M ) =/= 1 ) <-> ( ( b ` 1 ) = M /\ ( b ` M ) =/= 1 ) ) )
38	37, 6	elrab2 3366	. . . . . . . . . . . . . 14 |- ( b e. B <-> ( b e. A /\ ( ( b ` 1 ) = M /\ ( b ` M ) =/= 1 ) ) )
39	32, 38	sylib 208	. . . . . . . . . . . . 13 |- ( ( ph /\ b e. B ) -> ( b e. A /\ ( ( b ` 1 ) = M /\ ( b ` M ) =/= 1 ) ) )
40	39	simpld 475	. . . . . . . . . . . 12 |- ( ( ph /\ b e. B ) -> b e. A )
41		vex 3203	. . . . . . . . . . . . 13 |- b e. _V
42		f1oeq1 6127	. . . . . . . . . . . . . 14 |- ( f = b -> ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) <-> b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
43		fveq1 6190	. . . . . . . . . . . . . . . 16 |- ( f = b -> ( f ` y ) = ( b ` y ) )
44	43	neeq1d 2853	. . . . . . . . . . . . . . 15 |- ( f = b -> ( ( f ` y ) =/= y <-> ( b ` y ) =/= y ) )
45	44	ralbidv 2986	. . . . . . . . . . . . . 14 |- ( f = b -> ( A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y <-> A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y ) )
46	42, 45	anbi12d 747	. . . . . . . . . . . . 13 |- ( f = b -> ( ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) <-> ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y ) ) )
47	41, 46, 1	elab2 3354	. . . . . . . . . . . 12 |- ( b e. A <-> ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y ) )
48	40, 47	sylib 208	. . . . . . . . . . 11 |- ( ( ph /\ b e. B ) -> ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y ) )
49	48	simpld 475	. . . . . . . . . 10 |- ( ( ph /\ b e. B ) -> b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
50		f1oco 6159	. . . . . . . . . 10 |- ( ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) -> ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
51	31, 49, 50	syl2anc 693	. . . . . . . . 9 |- ( ( ph /\ b e. B ) -> ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
52		f1of1 6136	. . . . . . . . 9 |- ( ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) )
53		df-f1 5893	. . . . . . . . . 10 |- ( ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) <-> ( ( F o. b ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ Fun `' ( F o. b ) ) )
54	53	simprbi 480	. . . . . . . . 9 |- ( ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) -> Fun `' ( F o. b ) )
55	51, 52, 54	3syl 18	. . . . . . . 8 |- ( ( ph /\ b e. B ) -> Fun `' ( F o. b ) )
56		f1ofn 6138	. . . . . . . . . . 11 |- ( ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( F o. b ) Fn ( 1 ... ( N + 1 ) ) )
57		fnresdm 6000	. . . . . . . . . . 11 |- ( ( F o. b ) Fn ( 1 ... ( N + 1 ) ) -> ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) = ( F o. b ) )
58		f1oeq1 6127	. . . . . . . . . . 11 |- ( ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) = ( F o. b ) -> ( ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) <-> ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
59	51, 56, 57, 58	4syl 19	. . . . . . . . . 10 |- ( ( ph /\ b e. B ) -> ( ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) <-> ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
60	51, 59	mpbird 247	. . . . . . . . 9 |- ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
61		f1ofo 6144	. . . . . . . . 9 |- ( ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -onto-> ( 1 ... ( N + 1 ) ) )
62	60, 61	syl 17	. . . . . . . 8 |- ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -onto-> ( 1 ... ( N + 1 ) ) )
63		1ex 10035	. . . . . . . . . . 11 |- 1 e. _V
64	63, 63	f1osn 6176	. . . . . . . . . 10 |- { <. 1 , 1 >. } : { 1 } -1-1-onto-> { 1 }
65	51, 56	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ b e. B ) -> ( F o. b ) Fn ( 1 ... ( N + 1 ) ) )
66	22	peano2nnd 11037	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N + 1 ) e. NN )
67		nnuz 11723	. . . . . . . . . . . . . . . 16 |- NN = ( ZZ>= ` 1 )
68	66, 67	syl6eleq 2711	. . . . . . . . . . . . . . 15 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
69		eluzfz1 12348	. . . . . . . . . . . . . . 15 |- ( ( N + 1 ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( N + 1 ) ) )
70	68, 69	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> 1 e. ( 1 ... ( N + 1 ) ) )
71	70	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ b e. B ) -> 1 e. ( 1 ... ( N + 1 ) ) )
72		fnressn 6425	. . . . . . . . . . . . 13 |- ( ( ( F o. b ) Fn ( 1 ... ( N + 1 ) ) /\ 1 e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. b ) |` { 1 } ) = { <. 1 , ( ( F o. b ) ` 1 ) >. } )
73	65, 71, 72	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ph /\ b e. B ) -> ( ( F o. b ) |` { 1 } ) = { <. 1 , ( ( F o. b ) ` 1 ) >. } )
74		f1of 6137	. . . . . . . . . . . . . . . . 17 |- ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
75	49, 74	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ b e. B ) -> b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
76		fvco3 6275	. . . . . . . . . . . . . . . 16 |- ( ( b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ 1 e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. b ) ` 1 ) = ( F ` ( b ` 1 ) ) )
77	75, 71, 76	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ph /\ b e. B ) -> ( ( F o. b ) ` 1 ) = ( F ` ( b ` 1 ) ) )
78	39	simprd 479	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ b e. B ) -> ( ( b ` 1 ) = M /\ ( b ` M ) =/= 1 ) )
79	78	simpld 475	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ b e. B ) -> ( b ` 1 ) = M )
80	79	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( ( ph /\ b e. B ) -> ( F ` ( b ` 1 ) ) = ( F ` M ) )
81	29	simp3d 1075	. . . . . . . . . . . . . . . 16 |- ( ph -> ( F ` M ) = 1 )
82	81	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ b e. B ) -> ( F ` M ) = 1 )
83	77, 80, 82	3eqtrd 2660	. . . . . . . . . . . . . 14 |- ( ( ph /\ b e. B ) -> ( ( F o. b ) ` 1 ) = 1 )
84	83	opeq2d 4409	. . . . . . . . . . . . 13 |- ( ( ph /\ b e. B ) -> <. 1 , ( ( F o. b ) ` 1 ) >. = <. 1 , 1 >. )
85	84	sneqd 4189	. . . . . . . . . . . 12 |- ( ( ph /\ b e. B ) -> { <. 1 , ( ( F o. b ) ` 1 ) >. } = { <. 1 , 1 >. } )
86	73, 85	eqtrd 2656	. . . . . . . . . . 11 |- ( ( ph /\ b e. B ) -> ( ( F o. b ) |` { 1 } ) = { <. 1 , 1 >. } )
87		f1oeq1 6127	. . . . . . . . . . 11 |- ( ( ( F o. b ) |` { 1 } ) = { <. 1 , 1 >. } -> ( ( ( F o. b ) |` { 1 } ) : { 1 } -1-1-onto-> { 1 } <-> { <. 1 , 1 >. } : { 1 } -1-1-onto-> { 1 } ) )
88	86, 87	syl 17	. . . . . . . . . 10 |- ( ( ph /\ b e. B ) -> ( ( ( F o. b ) |` { 1 } ) : { 1 } -1-1-onto-> { 1 } <-> { <. 1 , 1 >. } : { 1 } -1-1-onto-> { 1 } ) )
89	64, 88	mpbiri 248	. . . . . . . . 9 |- ( ( ph /\ b e. B ) -> ( ( F o. b ) |` { 1 } ) : { 1 } -1-1-onto-> { 1 } )
90		f1ofo 6144	. . . . . . . . 9 |- ( ( ( F o. b ) |` { 1 } ) : { 1 } -1-1-onto-> { 1 } -> ( ( F o. b ) |` { 1 } ) : { 1 } -onto-> { 1 } )
91	89, 90	syl 17	. . . . . . . 8 |- ( ( ph /\ b e. B ) -> ( ( F o. b ) |` { 1 } ) : { 1 } -onto-> { 1 } )
92		resdif 6157	. . . . . . . 8 |- ( ( Fun `' ( F o. b ) /\ ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -onto-> ( 1 ... ( N + 1 ) ) /\ ( ( F o. b ) |` { 1 } ) : { 1 } -onto-> { 1 } ) -> ( ( F o. b ) |` ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) )
93	55, 62, 91, 92	syl3anc 1326	. . . . . . 7 |- ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) )
94		fzsplit 12367	. . . . . . . . . . . 12 |- ( 1 e. ( 1 ... ( N + 1 ) ) -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... ( N + 1 ) ) ) )
95	70, 94	syl 17	. . . . . . . . . . 11 |- ( ph -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... ( N + 1 ) ) ) )
96		1z 11407	. . . . . . . . . . . . 13 |- 1 e. ZZ
97		fzsn 12383	. . . . . . . . . . . . 13 |- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
98	96, 97	ax-mp 5	. . . . . . . . . . . 12 |- ( 1 ... 1 ) = { 1 }
99		1p1e2 11134	. . . . . . . . . . . . 13 |- ( 1 + 1 ) = 2
100	99	oveq1i 6660	. . . . . . . . . . . 12 |- ( ( 1 + 1 ) ... ( N + 1 ) ) = ( 2 ... ( N + 1 ) )
101	98, 100	uneq12i 3765	. . . . . . . . . . 11 |- ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... ( N + 1 ) ) ) = ( { 1 } u. ( 2 ... ( N + 1 ) ) )
102	95, 101	syl6req 2673	. . . . . . . . . 10 |- ( ph -> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) )
103	70	snssd 4340	. . . . . . . . . . 11 |- ( ph -> { 1 } C_ ( 1 ... ( N + 1 ) ) )
104		incom 3805	. . . . . . . . . . . 12 |- ( { 1 } i^i ( 2 ... ( N + 1 ) ) ) = ( ( 2 ... ( N + 1 ) ) i^i { 1 } )
105		1lt2 11194	. . . . . . . . . . . . . . 15 |- 1 < 2
106		1re 10039	. . . . . . . . . . . . . . . 16 |- 1 e. RR
107		2re 11090	. . . . . . . . . . . . . . . 16 |- 2 e. RR
108	106, 107	ltnlei 10158	. . . . . . . . . . . . . . 15 |- ( 1 < 2 <-> -. 2 <_ 1 )
109	105, 108	mpbi 220	. . . . . . . . . . . . . 14 |- -. 2 <_ 1
110		elfzle1 12344	. . . . . . . . . . . . . 14 |- ( 1 e. ( 2 ... ( N + 1 ) ) -> 2 <_ 1 )
111	109, 110	mto 188	. . . . . . . . . . . . 13 |- -. 1 e. ( 2 ... ( N + 1 ) )
112		disjsn 4246	. . . . . . . . . . . . 13 |- ( ( ( 2 ... ( N + 1 ) ) i^i { 1 } ) = (/) <-> -. 1 e. ( 2 ... ( N + 1 ) ) )
113	111, 112	mpbir 221	. . . . . . . . . . . 12 |- ( ( 2 ... ( N + 1 ) ) i^i { 1 } ) = (/)
114	104, 113	eqtri 2644	. . . . . . . . . . 11 |- ( { 1 } i^i ( 2 ... ( N + 1 ) ) ) = (/)
115		uneqdifeq 4057	. . . . . . . . . . 11 |- ( ( { 1 } C_ ( 1 ... ( N + 1 ) ) /\ ( { 1 } i^i ( 2 ... ( N + 1 ) ) ) = (/) ) -> ( ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) <-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) ) )
116	103, 114, 115	sylancl 694	. . . . . . . . . 10 |- ( ph -> ( ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) <-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) ) )
117	102, 116	mpbid 222	. . . . . . . . 9 |- ( ph -> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) )
118	117	adantr 481	. . . . . . . 8 |- ( ( ph /\ b e. B ) -> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) )
119		reseq2 5391	. . . . . . . . . 10 |- ( ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) -> ( ( F o. b ) |` ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) )
120		f1oeq1 6127	. . . . . . . . . 10 |- ( ( ( F o. b ) |` ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) -> ( ( ( F o. b ) |` ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) <-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) )
121	119, 120	syl 17	. . . . . . . . 9 |- ( ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) -> ( ( ( F o. b ) |` ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) <-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) )
122		f1oeq2 6128	. . . . . . . . 9 |- ( ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) -> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) <-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) )
123		f1oeq3 6129	. . . . . . . . 9 |- ( ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) -> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) <-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) ) )
124	121, 122, 123	3bitrd 294	. . . . . . . 8 |- ( ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) -> ( ( ( F o. b ) |` ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) <-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) ) )
125	118, 124	syl 17	. . . . . . 7 |- ( ( ph /\ b e. B ) -> ( ( ( F o. b ) |` ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) <-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) ) )
126	93, 125	mpbid 222	. . . . . 6 |- ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) )
127	75	adantr 481	. . . . . . . . 9 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
128		fzp1ss 12392	. . . . . . . . . . . 12 |- ( 1 e. ZZ -> ( ( 1 + 1 ) ... ( N + 1 ) ) C_ ( 1 ... ( N + 1 ) ) )
129	96, 128	ax-mp 5	. . . . . . . . . . 11 |- ( ( 1 + 1 ) ... ( N + 1 ) ) C_ ( 1 ... ( N + 1 ) )
130	100, 129	eqsstr3i 3636	. . . . . . . . . 10 |- ( 2 ... ( N + 1 ) ) C_ ( 1 ... ( N + 1 ) )
131		simpr 477	. . . . . . . . . 10 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> y e. ( 2 ... ( N + 1 ) ) )
132	130, 131	sseldi 3601	. . . . . . . . 9 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> y e. ( 1 ... ( N + 1 ) ) )
133		fvco3 6275	. . . . . . . . 9 |- ( ( b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. b ) ` y ) = ( F ` ( b ` y ) ) )
134	127, 132, 133	syl2anc 693	. . . . . . . 8 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( F o. b ) ` y ) = ( F ` ( b ` y ) ) )
135	20, 21, 1, 22, 23, 24, 25, 6, 26	subfacp1lem4 31165	. . . . . . . . . . . 12 |- ( ph -> `' F = F )
136	135	fveq1d 6193	. . . . . . . . . . 11 |- ( ph -> ( `' F ` y ) = ( F ` y ) )
137	136	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( `' F ` y ) = ( F ` y ) )
138	78	simprd 479	. . . . . . . . . . . . . . 15 |- ( ( ph /\ b e. B ) -> ( b ` M ) =/= 1 )
139	138, 82	neeqtrrd 2868	. . . . . . . . . . . . . 14 |- ( ( ph /\ b e. B ) -> ( b ` M ) =/= ( F ` M ) )
140	139	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( b ` M ) =/= ( F ` M ) )
141		fveq2 6191	. . . . . . . . . . . . . 14 |- ( y = M -> ( b ` y ) = ( b ` M ) )
142		fveq2 6191	. . . . . . . . . . . . . 14 |- ( y = M -> ( F ` y ) = ( F ` M ) )
143	141, 142	neeq12d 2855	. . . . . . . . . . . . 13 |- ( y = M -> ( ( b ` y ) =/= ( F ` y ) <-> ( b ` M ) =/= ( F ` M ) ) )
144	140, 143	syl5ibrcom 237	. . . . . . . . . . . 12 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( y = M -> ( b ` y ) =/= ( F ` y ) ) )
145	130	sseli 3599	. . . . . . . . . . . . . . . 16 |- ( y e. ( 2 ... ( N + 1 ) ) -> y e. ( 1 ... ( N + 1 ) ) )
146	48	simprd 479	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ b e. B ) -> A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y )
147	146	r19.21bi 2932	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ b e. B ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( b ` y ) =/= y )
148	145, 147	sylan2 491	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( b ` y ) =/= y )
149	148	adantrr 753	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ b e. B ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( b ` y ) =/= y )
150	25	eleq2i 2693	. . . . . . . . . . . . . . . . 17 |- ( y e. K <-> y e. ( ( 2 ... ( N + 1 ) ) \ { M } ) )
151		eldifsn 4317	. . . . . . . . . . . . . . . . 17 |- ( y e. ( ( 2 ... ( N + 1 ) ) \ { M } ) <-> ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) )
152	150, 151	bitri 264	. . . . . . . . . . . . . . . 16 |- ( y e. K <-> ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) )
153	20, 21, 1, 22, 23, 24, 25, 26, 28	subfacp1lem2b 31163	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. K ) -> ( F ` y ) = ( ( _I |` K ) ` y ) )
154		fvresi 6439	. . . . . . . . . . . . . . . . . 18 |- ( y e. K -> ( ( _I |` K ) ` y ) = y )
155	154	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. K ) -> ( ( _I |` K ) ` y ) = y )
156	153, 155	eqtrd 2656	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. K ) -> ( F ` y ) = y )
157	152, 156	sylan2br 493	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( F ` y ) = y )
158	157	adantlr 751	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ b e. B ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( F ` y ) = y )
159	149, 158	neeqtrrd 2868	. . . . . . . . . . . . 13 |- ( ( ( ph /\ b e. B ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( b ` y ) =/= ( F ` y ) )
160	159	expr 643	. . . . . . . . . . . 12 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( y =/= M -> ( b ` y ) =/= ( F ` y ) ) )
161	144, 160	pm2.61dne 2880	. . . . . . . . . . 11 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( b ` y ) =/= ( F ` y ) )
162	161	necomd 2849	. . . . . . . . . 10 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( F ` y ) =/= ( b ` y ) )
163	137, 162	eqnetrd 2861	. . . . . . . . 9 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( `' F ` y ) =/= ( b ` y ) )
164	31	adantr 481	. . . . . . . . . . 11 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
165		ffvelrn 6357	. . . . . . . . . . . 12 |- ( ( b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( b ` y ) e. ( 1 ... ( N + 1 ) ) )
166	75, 145, 165	syl2an 494	. . . . . . . . . . 11 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( b ` y ) e. ( 1 ... ( N + 1 ) ) )
167		f1ocnvfv 6534	. . . . . . . . . . 11 |- ( ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( b ` y ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( F ` ( b ` y ) ) = y -> ( `' F ` y ) = ( b ` y ) ) )
168	164, 166, 167	syl2anc 693	. . . . . . . . . 10 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( F ` ( b ` y ) ) = y -> ( `' F ` y ) = ( b ` y ) ) )
169	168	necon3d 2815	. . . . . . . . 9 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( `' F ` y ) =/= ( b ` y ) -> ( F ` ( b ` y ) ) =/= y ) )
170	163, 169	mpd 15	. . . . . . . 8 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( F ` ( b ` y ) ) =/= y )
171	134, 170	eqnetrd 2861	. . . . . . 7 |- ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( F o. b ) ` y ) =/= y )
172	171	ralrimiva 2966	. . . . . 6 |- ( ( ph /\ b e. B ) -> A. y e. ( 2 ... ( N + 1 ) ) ( ( F o. b ) ` y ) =/= y )
173		f1of 6137	. . . . . . . . . . . . 13 |- ( ( _I |` K ) : K -1-1-onto-> K -> ( _I |` K ) : K --> K )
174	27, 173	ax-mp 5	. . . . . . . . . . . 12 |- ( _I |` K ) : K --> K
175		difexg 4808	. . . . . . . . . . . . . 14 |- ( ( 2 ... ( N + 1 ) ) e. Fin -> ( ( 2 ... ( N + 1 ) ) \ { M } ) e. _V )
176	14, 175	ax-mp 5	. . . . . . . . . . . . 13 |- ( ( 2 ... ( N + 1 ) ) \ { M } ) e. _V
177	25, 176	eqeltri 2697	. . . . . . . . . . . 12 |- K e. _V
178		fex 6490	. . . . . . . . . . . 12 |- ( ( ( _I |` K ) : K --> K /\ K e. _V ) -> ( _I |` K ) e. _V )
179	174, 177, 178	mp2an 708	. . . . . . . . . . 11 |- ( _I |` K ) e. _V
180		prex 4909	. . . . . . . . . . 11 |- { <. 1 , M >. , <. M , 1 >. } e. _V
181	179, 180	unex 6956	. . . . . . . . . 10 |- ( ( _I |` K ) u. { <. 1 , M >. , <. M , 1 >. } ) e. _V
182	26, 181	eqeltri 2697	. . . . . . . . 9 |- F e. _V
183	182, 41	coex 7118	. . . . . . . 8 |- ( F o. b ) e. _V
184	183	resex 5443	. . . . . . 7 |- ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) e. _V
185		f1oeq1 6127	. . . . . . . 8 |- ( f = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) -> ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) <-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) ) )
186		fveq1 6190	. . . . . . . . . . 11 |- ( f = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) -> ( f ` y ) = ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) )
187		fvres 6207	. . . . . . . . . . 11 |- ( y e. ( 2 ... ( N + 1 ) ) -> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) = ( ( F o. b ) ` y ) )
188	186, 187	sylan9eq 2676	. . . . . . . . . 10 |- ( ( f = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( f ` y ) = ( ( F o. b ) ` y ) )
189	188	neeq1d 2853	. . . . . . . . 9 |- ( ( f = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( f ` y ) =/= y <-> ( ( F o. b ) ` y ) =/= y ) )
190	189	ralbidva 2985	. . . . . . . 8 |- ( f = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) -> ( A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y <-> A. y e. ( 2 ... ( N + 1 ) ) ( ( F o. b ) ` y ) =/= y ) )
191	185, 190	anbi12d 747	. . . . . . 7 |- ( f = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) -> ( ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) <-> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( ( F o. b ) ` y ) =/= y ) ) )
192	184, 191, 13	elab2 3354	. . . . . 6 |- ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) e. C <-> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( ( F o. b ) ` y ) =/= y ) )
193	126, 172, 192	sylanbrc 698	. . . . 5 |- ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) e. C )
194	193	ex 450	. . . 4 |- ( ph -> ( b e. B -> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) e. C ) )
195	30	adantr 481	. . . . . . . 8 |- ( ( ph /\ c e. C ) -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
196		simpr 477	. . . . . . . . . . . 12 |- ( ( ph /\ c e. C ) -> c e. C )
197		vex 3203	. . . . . . . . . . . . 13 |- c e. _V
198		f1oeq1 6127	. . . . . . . . . . . . . 14 |- ( f = c -> ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) <-> c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) ) )
199		fveq1 6190	. . . . . . . . . . . . . . . 16 |- ( f = c -> ( f ` y ) = ( c ` y ) )
200	199	neeq1d 2853	. . . . . . . . . . . . . . 15 |- ( f = c -> ( ( f ` y ) =/= y <-> ( c ` y ) =/= y ) )
201	200	ralbidv 2986	. . . . . . . . . . . . . 14 |- ( f = c -> ( A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y <-> A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y ) )
202	198, 201	anbi12d 747	. . . . . . . . . . . . 13 |- ( f = c -> ( ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) <-> ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y ) ) )
203	197, 202, 13	elab2 3354	. . . . . . . . . . . 12 |- ( c e. C <-> ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y ) )
204	196, 203	sylib 208	. . . . . . . . . . 11 |- ( ( ph /\ c e. C ) -> ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y ) )
205	204	simpld 475	. . . . . . . . . 10 |- ( ( ph /\ c e. C ) -> c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) )
206		f1oun 6156	. . . . . . . . . . 11 |- ( ( ( { <. 1 , 1 >. } : { 1 } -1-1-onto-> { 1 } /\ c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) ) /\ ( ( { 1 } i^i ( 2 ... ( N + 1 ) ) ) = (/) /\ ( { 1 } i^i ( 2 ... ( N + 1 ) ) ) = (/) ) ) -> ( { <. 1 , 1 >. } u. c ) : ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) )
207	114, 114, 206	mpanr12 721	. . . . . . . . . 10 |- ( ( { <. 1 , 1 >. } : { 1 } -1-1-onto-> { 1 } /\ c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) ) -> ( { <. 1 , 1 >. } u. c ) : ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) )
208	64, 205, 207	sylancr 695	. . . . . . . . 9 |- ( ( ph /\ c e. C ) -> ( { <. 1 , 1 >. } u. c ) : ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) )
209		f1oeq2 6128	. . . . . . . . . . . 12 |- ( ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) -> ( ( { <. 1 , 1 >. } u. c ) : ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) <-> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) ) )
210		f1oeq3 6129	. . . . . . . . . . . 12 |- ( ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) -> ( ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) <-> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
211	209, 210	bitrd 268	. . . . . . . . . . 11 |- ( ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) -> ( ( { <. 1 , 1 >. } u. c ) : ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) <-> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
212	102, 211	syl 17	. . . . . . . . . 10 |- ( ph -> ( ( { <. 1 , 1 >. } u. c ) : ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) <-> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
213	212	biimpa 501	. . . . . . . . 9 |- ( ( ph /\ ( { <. 1 , 1 >. } u. c ) : ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
214	208, 213	syldan 487	. . . . . . . 8 |- ( ( ph /\ c e. C ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
215		f1oco 6159	. . . . . . . 8 |- ( ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) -> ( F o. ( { <. 1 , 1 >. } u. c ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
216	195, 214, 215	syl2anc 693	. . . . . . 7 |- ( ( ph /\ c e. C ) -> ( F o. ( { <. 1 , 1 >. } u. c ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
217		f1of 6137	. . . . . . . . . . 11 |- ( ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
218	214, 217	syl 17	. . . . . . . . . 10 |- ( ( ph /\ c e. C ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
219		fvco3 6275	. . . . . . . . . 10 |- ( ( ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) = ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
220	218, 219	sylan 488	. . . . . . . . 9 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) = ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
221	136	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( `' F ` y ) = ( F ` y ) )
222		simpr 477	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> y e. ( 1 ... ( N + 1 ) ) )
223	102	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) )
224	222, 223	eleqtrrd 2704	. . . . . . . . . . . . 13 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> y e. ( { 1 } u. ( 2 ... ( N + 1 ) ) ) )
225		elun 3753	. . . . . . . . . . . . 13 |- ( y e. ( { 1 } u. ( 2 ... ( N + 1 ) ) ) <-> ( y e. { 1 } \/ y e. ( 2 ... ( N + 1 ) ) ) )
226	224, 225	sylib 208	. . . . . . . . . . . 12 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( y e. { 1 } \/ y e. ( 2 ... ( N + 1 ) ) ) )
227		nelne2 2891	. . . . . . . . . . . . . . . . . 18 |- ( ( M e. ( 2 ... ( N + 1 ) ) /\ -. 1 e. ( 2 ... ( N + 1 ) ) ) -> M =/= 1 )
228	23, 111, 227	sylancl 694	. . . . . . . . . . . . . . . . 17 |- ( ph -> M =/= 1 )
229	228	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. C ) -> M =/= 1 )
230	29	simp2d 1074	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( F ` 1 ) = M )
231	230	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. C ) -> ( F ` 1 ) = M )
232		f1ofun 6139	. . . . . . . . . . . . . . . . . . 19 |- ( ( { <. 1 , 1 >. } u. c ) : ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -> Fun ( { <. 1 , 1 >. } u. c ) )
233	208, 232	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ c e. C ) -> Fun ( { <. 1 , 1 >. } u. c ) )
234		ssun1 3776	. . . . . . . . . . . . . . . . . . 19 |- { <. 1 , 1 >. } C_ ( { <. 1 , 1 >. } u. c )
235	63	snid 4208	. . . . . . . . . . . . . . . . . . . 20 |- 1 e. { 1 }
236	63	dmsnop 5609	. . . . . . . . . . . . . . . . . . . 20 |- dom { <. 1 , 1 >. } = { 1 }
237	235, 236	eleqtrri 2700	. . . . . . . . . . . . . . . . . . 19 |- 1 e. dom { <. 1 , 1 >. }
238		funssfv 6209	. . . . . . . . . . . . . . . . . . 19 |- ( ( Fun ( { <. 1 , 1 >. } u. c ) /\ { <. 1 , 1 >. } C_ ( { <. 1 , 1 >. } u. c ) /\ 1 e. dom { <. 1 , 1 >. } ) -> ( ( { <. 1 , 1 >. } u. c ) ` 1 ) = ( { <. 1 , 1 >. } ` 1 ) )
239	234, 237, 238	mp3an23 1416	. . . . . . . . . . . . . . . . . 18 |- ( Fun ( { <. 1 , 1 >. } u. c ) -> ( ( { <. 1 , 1 >. } u. c ) ` 1 ) = ( { <. 1 , 1 >. } ` 1 ) )
240	233, 239	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ c e. C ) -> ( ( { <. 1 , 1 >. } u. c ) ` 1 ) = ( { <. 1 , 1 >. } ` 1 ) )
241	63, 63	fvsn 6446	. . . . . . . . . . . . . . . . 17 |- ( { <. 1 , 1 >. } ` 1 ) = 1
242	240, 241	syl6eq 2672	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. C ) -> ( ( { <. 1 , 1 >. } u. c ) ` 1 ) = 1 )
243	229, 231, 242	3netr4d 2871	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. C ) -> ( F ` 1 ) =/= ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
244		elsni 4194	. . . . . . . . . . . . . . . . 17 |- ( y e. { 1 } -> y = 1 )
245	244	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( y e. { 1 } -> ( F ` y ) = ( F ` 1 ) )
246	244	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( y e. { 1 } -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
247	245, 246	neeq12d 2855	. . . . . . . . . . . . . . 15 |- ( y e. { 1 } -> ( ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> ( F ` 1 ) =/= ( ( { <. 1 , 1 >. } u. c ) ` 1 ) ) )
248	243, 247	syl5ibrcom 237	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. C ) -> ( y e. { 1 } -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
249	248	imp 445	. . . . . . . . . . . . 13 |- ( ( ( ph /\ c e. C ) /\ y e. { 1 } ) -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
250	233	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> Fun ( { <. 1 , 1 >. } u. c ) )
251		ssun2 3777	. . . . . . . . . . . . . . . . 17 |- c C_ ( { <. 1 , 1 >. } u. c )
252	251	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> c C_ ( { <. 1 , 1 >. } u. c ) )
253		f1odm 6141	. . . . . . . . . . . . . . . . . . 19 |- ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) -> dom c = ( 2 ... ( N + 1 ) ) )
254	205, 253	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ c e. C ) -> dom c = ( 2 ... ( N + 1 ) ) )
255	254	eleq2d 2687	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ c e. C ) -> ( y e. dom c <-> y e. ( 2 ... ( N + 1 ) ) ) )
256	255	biimpar 502	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> y e. dom c )
257		funssfv 6209	. . . . . . . . . . . . . . . 16 |- ( ( Fun ( { <. 1 , 1 >. } u. c ) /\ c C_ ( { <. 1 , 1 >. } u. c ) /\ y e. dom c ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( c ` y ) )
258	250, 252, 256, 257	syl3anc 1326	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( c ` y ) )
259		f1of 6137	. . . . . . . . . . . . . . . . . . . . . 22 |- ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) -> c : ( 2 ... ( N + 1 ) ) --> ( 2 ... ( N + 1 ) ) )
260	205, 259	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ c e. C ) -> c : ( 2 ... ( N + 1 ) ) --> ( 2 ... ( N + 1 ) ) )
261	23	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ c e. C ) -> M e. ( 2 ... ( N + 1 ) ) )
262	260, 261	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ c e. C ) -> ( c ` M ) e. ( 2 ... ( N + 1 ) ) )
263		nelne2 2891	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( c ` M ) e. ( 2 ... ( N + 1 ) ) /\ -. 1 e. ( 2 ... ( N + 1 ) ) ) -> ( c ` M ) =/= 1 )
264	262, 111, 263	sylancl 694	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ c e. C ) -> ( c ` M ) =/= 1 )
265	264	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( c ` M ) =/= 1 )
266	81	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( F ` M ) = 1 )
267	265, 266	neeqtrrd 2868	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( c ` M ) =/= ( F ` M ) )
268		fveq2 6191	. . . . . . . . . . . . . . . . . 18 |- ( y = M -> ( c ` y ) = ( c ` M ) )
269	268, 142	neeq12d 2855	. . . . . . . . . . . . . . . . 17 |- ( y = M -> ( ( c ` y ) =/= ( F ` y ) <-> ( c ` M ) =/= ( F ` M ) ) )
270	267, 269	syl5ibrcom 237	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( y = M -> ( c ` y ) =/= ( F ` y ) ) )
271	204	simprd 479	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ c e. C ) -> A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y )
272	271	r19.21bi 2932	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( c ` y ) =/= y )
273	272	adantrr 753	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. C ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( c ` y ) =/= y )
274	157	adantlr 751	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. C ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( F ` y ) = y )
275	273, 274	neeqtrrd 2868	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ c e. C ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( c ` y ) =/= ( F ` y ) )
276	275	expr 643	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( y =/= M -> ( c ` y ) =/= ( F ` y ) ) )
277	270, 276	pm2.61dne 2880	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( c ` y ) =/= ( F ` y ) )
278	258, 277	eqnetrd 2861	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) =/= ( F ` y ) )
279	278	necomd 2849	. . . . . . . . . . . . 13 |- ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
280	249, 279	jaodan 826	. . . . . . . . . . . 12 |- ( ( ( ph /\ c e. C ) /\ ( y e. { 1 } \/ y e. ( 2 ... ( N + 1 ) ) ) ) -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
281	226, 280	syldan 487	. . . . . . . . . . 11 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
282	221, 281	eqnetrd 2861	. . . . . . . . . 10 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( `' F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
283	195	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
284	218	ffvelrnda 6359	. . . . . . . . . . . 12 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) e. ( 1 ... ( N + 1 ) ) )
285		f1ocnvfv 6534	. . . . . . . . . . . 12 |- ( ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( ( { <. 1 , 1 >. } u. c ) ` y ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) = y -> ( `' F ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
286	283, 284, 285	syl2anc 693	. . . . . . . . . . 11 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) = y -> ( `' F ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
287	286	necon3d 2815	. . . . . . . . . 10 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( `' F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) -> ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) =/= y ) )
288	282, 287	mpd 15	. . . . . . . . 9 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) =/= y )
289	220, 288	eqnetrd 2861	. . . . . . . 8 |- ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) =/= y )
290	289	ralrimiva 2966	. . . . . . 7 |- ( ( ph /\ c e. C ) -> A. y e. ( 1 ... ( N + 1 ) ) ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) =/= y )
291		snex 4908	. . . . . . . . . 10 |- { <. 1 , 1 >. } e. _V
292	291, 197	unex 6956	. . . . . . . . 9 |- ( { <. 1 , 1 >. } u. c ) e. _V
293	182, 292	coex 7118	. . . . . . . 8 |- ( F o. ( { <. 1 , 1 >. } u. c ) ) e. _V
294		f1oeq1 6127	. . . . . . . . 9 |- ( f = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) <-> ( F o. ( { <. 1 , 1 >. } u. c ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
295		fveq1 6190	. . . . . . . . . . 11 |- ( f = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( f ` y ) = ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) )
296	295	neeq1d 2853	. . . . . . . . . 10 |- ( f = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( ( f ` y ) =/= y <-> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) =/= y ) )
297	296	ralbidv 2986	. . . . . . . . 9 |- ( f = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y <-> A. y e. ( 1 ... ( N + 1 ) ) ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) =/= y ) )
298	294, 297	anbi12d 747	. . . . . . . 8 |- ( f = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) <-> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) =/= y ) ) )
299	293, 298, 1	elab2 3354	. . . . . . 7 |- ( ( F o. ( { <. 1 , 1 >. } u. c ) ) e. A <-> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) =/= y ) )
300	216, 290, 299	sylanbrc 698	. . . . . 6 |- ( ( ph /\ c e. C ) -> ( F o. ( { <. 1 , 1 >. } u. c ) ) e. A )
301	70	adantr 481	. . . . . . . . 9 |- ( ( ph /\ c e. C ) -> 1 e. ( 1 ... ( N + 1 ) ) )
302		fvco3 6275	. . . . . . . . 9 |- ( ( ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ 1 e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = ( F ` ( ( { <. 1 , 1 >. } u. c ) ` 1 ) ) )
303	218, 301, 302	syl2anc 693	. . . . . . . 8 |- ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = ( F ` ( ( { <. 1 , 1 >. } u. c ) ` 1 ) ) )
304	242	fveq2d 6195	. . . . . . . 8 |- ( ( ph /\ c e. C ) -> ( F ` ( ( { <. 1 , 1 >. } u. c ) ` 1 ) ) = ( F ` 1 ) )
305	303, 304, 231	3eqtrd 2660	. . . . . . 7 |- ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = M )
306	130, 23	sseldi 3601	. . . . . . . . . . 11 |- ( ph -> M e. ( 1 ... ( N + 1 ) ) )
307	306	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ c e. C ) -> M e. ( 1 ... ( N + 1 ) ) )
308		fvco3 6275	. . . . . . . . . 10 |- ( ( ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ M e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) = ( F ` ( ( { <. 1 , 1 >. } u. c ) ` M ) ) )
309	218, 307, 308	syl2anc 693	. . . . . . . . 9 |- ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) = ( F ` ( ( { <. 1 , 1 >. } u. c ) ` M ) ) )
310	251	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ c e. C ) -> c C_ ( { <. 1 , 1 >. } u. c ) )
311	261, 254	eleqtrrd 2704	. . . . . . . . . . 11 |- ( ( ph /\ c e. C ) -> M e. dom c )
312		funssfv 6209	. . . . . . . . . . 11 |- ( ( Fun ( { <. 1 , 1 >. } u. c ) /\ c C_ ( { <. 1 , 1 >. } u. c ) /\ M e. dom c ) -> ( ( { <. 1 , 1 >. } u. c ) ` M ) = ( c ` M ) )
313	233, 310, 311, 312	syl3anc 1326	. . . . . . . . . 10 |- ( ( ph /\ c e. C ) -> ( ( { <. 1 , 1 >. } u. c ) ` M ) = ( c ` M ) )
314	313	fveq2d 6195	. . . . . . . . 9 |- ( ( ph /\ c e. C ) -> ( F ` ( ( { <. 1 , 1 >. } u. c ) ` M ) ) = ( F ` ( c ` M ) ) )
315	309, 314	eqtrd 2656	. . . . . . . 8 |- ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) = ( F ` ( c ` M ) ) )
316	135	fveq1d 6193	. . . . . . . . . . . 12 |- ( ph -> ( `' F ` 1 ) = ( F ` 1 ) )
317	316, 230	eqtrd 2656	. . . . . . . . . . 11 |- ( ph -> ( `' F ` 1 ) = M )
318	317	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ c e. C ) -> ( `' F ` 1 ) = M )
319		id 22	. . . . . . . . . . . . . 14 |- ( y = M -> y = M )
320	268, 319	neeq12d 2855	. . . . . . . . . . . . 13 |- ( y = M -> ( ( c ` y ) =/= y <-> ( c ` M ) =/= M ) )
321	320	rspcv 3305	. . . . . . . . . . . 12 |- ( M e. ( 2 ... ( N + 1 ) ) -> ( A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y -> ( c ` M ) =/= M ) )
322	261, 271, 321	sylc 65	. . . . . . . . . . 11 |- ( ( ph /\ c e. C ) -> ( c ` M ) =/= M )
323	322	necomd 2849	. . . . . . . . . 10 |- ( ( ph /\ c e. C ) -> M =/= ( c ` M ) )
324	318, 323	eqnetrd 2861	. . . . . . . . 9 |- ( ( ph /\ c e. C ) -> ( `' F ` 1 ) =/= ( c ` M ) )
325	130, 262	sseldi 3601	. . . . . . . . . . 11 |- ( ( ph /\ c e. C ) -> ( c ` M ) e. ( 1 ... ( N + 1 ) ) )
326		f1ocnvfv 6534	. . . . . . . . . . 11 |- ( ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( c ` M ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( F ` ( c ` M ) ) = 1 -> ( `' F ` 1 ) = ( c ` M ) ) )
327	195, 325, 326	syl2anc 693	. . . . . . . . . 10 |- ( ( ph /\ c e. C ) -> ( ( F ` ( c ` M ) ) = 1 -> ( `' F ` 1 ) = ( c ` M ) ) )
328	327	necon3d 2815	. . . . . . . . 9 |- ( ( ph /\ c e. C ) -> ( ( `' F ` 1 ) =/= ( c ` M ) -> ( F ` ( c ` M ) ) =/= 1 ) )
329	324, 328	mpd 15	. . . . . . . 8 |- ( ( ph /\ c e. C ) -> ( F ` ( c ` M ) ) =/= 1 )
330	315, 329	eqnetrd 2861	. . . . . . 7 |- ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) =/= 1 )
331	305, 330	jca 554	. . . . . 6 |- ( ( ph /\ c e. C ) -> ( ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = M /\ ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) =/= 1 ) )
332		fveq1 6190	. . . . . . . . 9 |- ( g = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( g ` 1 ) = ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) )
333	332	eqeq1d 2624	. . . . . . . 8 |- ( g = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( ( g ` 1 ) = M <-> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = M ) )
334		fveq1 6190	. . . . . . . . 9 |- ( g = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( g ` M ) = ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) )
335	334	neeq1d 2853	. . . . . . . 8 |- ( g = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( ( g ` M ) =/= 1 <-> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) =/= 1 ) )
336	333, 335	anbi12d 747	. . . . . . 7 |- ( g = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( ( ( g ` 1 ) = M /\ ( g ` M ) =/= 1 ) <-> ( ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = M /\ ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) =/= 1 ) ) )
337	336, 6	elrab2 3366	. . . . . 6 |- ( ( F o. ( { <. 1 , 1 >. } u. c ) ) e. B <-> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) e. A /\ ( ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = M /\ ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) =/= 1 ) ) )
338	300, 331, 337	sylanbrc 698	. . . . 5 |- ( ( ph /\ c e. C ) -> ( F o. ( { <. 1 , 1 >. } u. c ) ) e. B )
339	338	ex 450	. . . 4 |- ( ph -> ( c e. C -> ( F o. ( { <. 1 , 1 >. } u. c ) ) e. B ) )
340	30	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
341		f1of1 6136	. . . . . . . 8 |- ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> F : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) )
342	340, 341	syl 17	. . . . . . 7 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> F : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) )
343		f1of 6137	. . . . . . . . 9 |- ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> F : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
344	340, 343	syl 17	. . . . . . . 8 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> F : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
345	75	adantrr 753	. . . . . . . 8 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
346		fco 6058	. . . . . . . 8 |- ( ( F : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) ) -> ( F o. b ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
347	344, 345, 346	syl2anc 693	. . . . . . 7 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( F o. b ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
348	218	adantrl 752	. . . . . . 7 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
349		cocan1 6546	. . . . . . 7 |- ( ( F : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) /\ ( F o. b ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) ) -> ( ( F o. ( F o. b ) ) = ( F o. ( { <. 1 , 1 >. } u. c ) ) <-> ( F o. b ) = ( { <. 1 , 1 >. } u. c ) ) )
350	342, 347, 348, 349	syl3anc 1326	. . . . . 6 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. ( F o. b ) ) = ( F o. ( { <. 1 , 1 >. } u. c ) ) <-> ( F o. b ) = ( { <. 1 , 1 >. } u. c ) ) )
351		coass 5654	. . . . . . . 8 |- ( ( F o. F ) o. b ) = ( F o. ( F o. b ) )
352	135	coeq1d 5283	. . . . . . . . . . . 12 |- ( ph -> ( `' F o. F ) = ( F o. F ) )
353		f1ococnv1 6165	. . . . . . . . . . . . 13 |- ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( `' F o. F ) = ( _I |` ( 1 ... ( N + 1 ) ) ) )
354	30, 353	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( `' F o. F ) = ( _I |` ( 1 ... ( N + 1 ) ) ) )
355	352, 354	eqtr3d 2658	. . . . . . . . . . 11 |- ( ph -> ( F o. F ) = ( _I |` ( 1 ... ( N + 1 ) ) ) )
356	355	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( F o. F ) = ( _I |` ( 1 ... ( N + 1 ) ) ) )
357	356	coeq1d 5283	. . . . . . . . 9 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. F ) o. b ) = ( ( _I |` ( 1 ... ( N + 1 ) ) ) o. b ) )
358		fcoi2 6079	. . . . . . . . . 10 |- ( b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) -> ( ( _I |` ( 1 ... ( N + 1 ) ) ) o. b ) = b )
359	345, 358	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( _I |` ( 1 ... ( N + 1 ) ) ) o. b ) = b )
360	357, 359	eqtrd 2656	. . . . . . . 8 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. F ) o. b ) = b )
361	351, 360	syl5eqr 2670	. . . . . . 7 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( F o. ( F o. b ) ) = b )
362	361	eqeq1d 2624	. . . . . 6 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. ( F o. b ) ) = ( F o. ( { <. 1 , 1 >. } u. c ) ) <-> b = ( F o. ( { <. 1 , 1 >. } u. c ) ) ) )
363	83	adantrr 753	. . . . . . . . . . . . 13 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) ` 1 ) = 1 )
364	242	adantrl 752	. . . . . . . . . . . . 13 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` 1 ) = 1 )
365	363, 364	eqtr4d 2659	. . . . . . . . . . . 12 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) ` 1 ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
366		fveq2 6191	. . . . . . . . . . . . . 14 |- ( y = 1 -> ( ( F o. b ) ` y ) = ( ( F o. b ) ` 1 ) )
367		fveq2 6191	. . . . . . . . . . . . . 14 |- ( y = 1 -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
368	366, 367	eqeq12d 2637	. . . . . . . . . . . . 13 |- ( y = 1 -> ( ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> ( ( F o. b ) ` 1 ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) ) )
369	63, 368	ralsn 4222	. . . . . . . . . . . 12 |- ( A. y e. { 1 } ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> ( ( F o. b ) ` 1 ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
370	365, 369	sylibr 224	. . . . . . . . . . 11 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> A. y e. { 1 } ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) )
371	370	biantrurd 529	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( A. y e. ( 2 ... ( N + 1 ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> ( A. y e. { 1 } ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) ) ) )
372		ralunb 3794	. . . . . . . . . 10 |- ( A. y e. ( { 1 } u. ( 2 ... ( N + 1 ) ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> ( A. y e. { 1 } ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
373	371, 372	syl6bbr 278	. . . . . . . . 9 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( A. y e. ( 2 ... ( N + 1 ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> A. y e. ( { 1 } u. ( 2 ... ( N + 1 ) ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
374	187	adantl 482	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( b e. B /\ c e. C ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) = ( ( F o. b ) ` y ) )
375	374	eqcomd 2628	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b e. B /\ c e. C ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( F o. b ) ` y ) = ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) )
376	258	adantlrl 756	. . . . . . . . . . 11 |- ( ( ( ph /\ ( b e. B /\ c e. C ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( c ` y ) )
377	375, 376	eqeq12d 2637	. . . . . . . . . 10 |- ( ( ( ph /\ ( b e. B /\ c e. C ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) = ( c ` y ) ) )
378	377	ralbidva 2985	. . . . . . . . 9 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( A. y e. ( 2 ... ( N + 1 ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> A. y e. ( 2 ... ( N + 1 ) ) ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) = ( c ` y ) ) )
379	102	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) )
380	379	raleqdv 3144	. . . . . . . . 9 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( A. y e. ( { 1 } u. ( 2 ... ( N + 1 ) ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> A. y e. ( 1 ... ( N + 1 ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
381	373, 378, 380	3bitr3rd 299	. . . . . . . 8 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( A. y e. ( 1 ... ( N + 1 ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> A. y e. ( 2 ... ( N + 1 ) ) ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) = ( c ` y ) ) )
382	65	adantrr 753	. . . . . . . . 9 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( F o. b ) Fn ( 1 ... ( N + 1 ) ) )
383	214	adantrl 752	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
384		f1ofn 6138	. . . . . . . . . 10 |- ( ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( { <. 1 , 1 >. } u. c ) Fn ( 1 ... ( N + 1 ) ) )
385	383, 384	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( { <. 1 , 1 >. } u. c ) Fn ( 1 ... ( N + 1 ) ) )
386		eqfnfv 6311	. . . . . . . . 9 |- ( ( ( F o. b ) Fn ( 1 ... ( N + 1 ) ) /\ ( { <. 1 , 1 >. } u. c ) Fn ( 1 ... ( N + 1 ) ) ) -> ( ( F o. b ) = ( { <. 1 , 1 >. } u. c ) <-> A. y e. ( 1 ... ( N + 1 ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
387	382, 385, 386	syl2anc 693	. . . . . . . 8 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) = ( { <. 1 , 1 >. } u. c ) <-> A. y e. ( 1 ... ( N + 1 ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
388		fnssres 6004	. . . . . . . . . 10 |- ( ( ( F o. b ) Fn ( 1 ... ( N + 1 ) ) /\ ( 2 ... ( N + 1 ) ) C_ ( 1 ... ( N + 1 ) ) ) -> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) Fn ( 2 ... ( N + 1 ) ) )
389	382, 130, 388	sylancl 694	. . . . . . . . 9 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) Fn ( 2 ... ( N + 1 ) ) )
390	205	adantrl 752	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) )
391		f1ofn 6138	. . . . . . . . . 10 |- ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) -> c Fn ( 2 ... ( N + 1 ) ) )
392	390, 391	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> c Fn ( 2 ... ( N + 1 ) ) )
393		eqfnfv 6311	. . . . . . . . 9 |- ( ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) Fn ( 2 ... ( N + 1 ) ) /\ c Fn ( 2 ... ( N + 1 ) ) ) -> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) = c <-> A. y e. ( 2 ... ( N + 1 ) ) ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) = ( c ` y ) ) )
394	389, 392, 393	syl2anc 693	. . . . . . . 8 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) = c <-> A. y e. ( 2 ... ( N + 1 ) ) ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) = ( c ` y ) ) )
395	381, 387, 394	3bitr4d 300	. . . . . . 7 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) = ( { <. 1 , 1 >. } u. c ) <-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) = c ) )
396		eqcom 2629	. . . . . . 7 |- ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) = c <-> c = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) )
397	395, 396	syl6bb 276	. . . . . 6 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) = ( { <. 1 , 1 >. } u. c ) <-> c = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ) )
398	350, 362, 397	3bitr3d 298	. . . . 5 |- ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b = ( F o. ( { <. 1 , 1 >. } u. c ) ) <-> c = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ) )
399	398	ex 450	. . . 4 |- ( ph -> ( ( b e. B /\ c e. C ) -> ( b = ( F o. ( { <. 1 , 1 >. } u. c ) ) <-> c = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ) ) )
400	12, 19, 194, 339, 399	en3d 7992	. . 3 |- ( ph -> B ~~ C )
401		hashen 13135	. . . 4 |- ( ( B e. Fin /\ C e. Fin ) -> ( ( # ` B ) = ( # ` C ) <-> B ~~ C ) )
402	10, 17, 401	mp2an 708	. . 3 |- ( ( # ` B ) = ( # ` C ) <-> B ~~ C )
403	400, 402	sylibr 224	. 2 |- ( ph -> ( # ` B ) = ( # ` C ) )
404	20, 21	derangen2 31156	. . . . 5 |- ( ( 2 ... ( N + 1 ) ) e. Fin -> ( D ` ( 2 ... ( N + 1 ) ) ) = ( S ` ( # ` ( 2 ... ( N + 1 ) ) ) ) )
405	20	derangval 31149	. . . . . 6 |- ( ( 2 ... ( N + 1 ) ) e. Fin -> ( D ` ( 2 ... ( N + 1 ) ) ) = ( # ` { f | ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) } ) )
406	13	fveq2i 6194	. . . . . 6 |- ( # ` C ) = ( # ` { f | ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) } )
407	405, 406	syl6eqr 2674	. . . . 5 |- ( ( 2 ... ( N + 1 ) ) e. Fin -> ( D ` ( 2 ... ( N + 1 ) ) ) = ( # ` C ) )
408	404, 407	eqtr3d 2658	. . . 4 |- ( ( 2 ... ( N + 1 ) ) e. Fin -> ( S ` ( # ` ( 2 ... ( N + 1 ) ) ) ) = ( # ` C ) )
409	14, 408	ax-mp 5	. . 3 |- ( S ` ( # ` ( 2 ... ( N + 1 ) ) ) ) = ( # ` C )
410	22, 67	syl6eleq 2711	. . . . . . . 8 |- ( ph -> N e. ( ZZ>= ` 1 ) )
411		eluzp1p1 11713	. . . . . . . 8 |- ( N e. ( ZZ>= ` 1 ) -> ( N + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
412	410, 411	syl 17	. . . . . . 7 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
413		df-2 11079	. . . . . . . 8 |- 2 = ( 1 + 1 )
414	413	fveq2i 6194	. . . . . . 7 |- ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
415	412, 414	syl6eleqr 2712	. . . . . 6 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 2 ) )
416		hashfz 13214	. . . . . 6 |- ( ( N + 1 ) e. ( ZZ>= ` 2 ) -> ( # ` ( 2 ... ( N + 1 ) ) ) = ( ( ( N + 1 ) - 2 ) + 1 ) )
417	415, 416	syl 17	. . . . 5 |- ( ph -> ( # ` ( 2 ... ( N + 1 ) ) ) = ( ( ( N + 1 ) - 2 ) + 1 ) )
418	66	nncnd 11036	. . . . . 6 |- ( ph -> ( N + 1 ) e. CC )
419		2cnd 11093	. . . . . 6 |- ( ph -> 2 e. CC )
420		1cnd 10056	. . . . . 6 |- ( ph -> 1 e. CC )
421	418, 419, 420	subsubd 10420	. . . . 5 |- ( ph -> ( ( N + 1 ) - ( 2 - 1 ) ) = ( ( ( N + 1 ) - 2 ) + 1 ) )
422		2m1e1 11135	. . . . . . 7 |- ( 2 - 1 ) = 1
423	422	oveq2i 6661	. . . . . 6 |- ( ( N + 1 ) - ( 2 - 1 ) ) = ( ( N + 1 ) - 1 )
424	22	nncnd 11036	. . . . . . 7 |- ( ph -> N e. CC )
425		ax-1cn 9994	. . . . . . 7 |- 1 e. CC
426		pncan 10287	. . . . . . 7 |- ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
427	424, 425, 426	sylancl 694	. . . . . 6 |- ( ph -> ( ( N + 1 ) - 1 ) = N )
428	423, 427	syl5eq 2668	. . . . 5 |- ( ph -> ( ( N + 1 ) - ( 2 - 1 ) ) = N )
429	417, 421, 428	3eqtr2d 2662	. . . 4 |- ( ph -> ( # ` ( 2 ... ( N + 1 ) ) ) = N )
430	429	fveq2d 6195	. . 3 |- ( ph -> ( S ` ( # ` ( 2 ... ( N + 1 ) ) ) ) = ( S ` N ) )
431	409, 430	syl5eqr 2670	. 2 |- ( ph -> ( # ` C ) = ( S ` N ) )
432	403, 431	eqtrd 2656	1 |- ( ph -> ( # ` B ) = ( S ` N ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   {crab 2916   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   {csn 4177   {cpr 4179   <.cop 4183   class class class wbr 4653   |-> cmpt 4729   _I cid 5023   `'ccnv 5113   dom cdm 5114   |` cres 5116   o. ccom 5118   Fun wfun 5882   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   ~~ cen 7952   Fincfn 7955   CCcc 9934   1c1 9937   + caddc 9939   < clt 10074   <_ cle 10075   - cmin 10266   NNcn 11020   2c2 11070   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326   #chash 13117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-n0 11293  df-xnn0 11364  df-z 11378  df-uz 11688  df-fz 12327  df-hash 13118

This theorem is referenced by:  subfacp1lem6  31167