Metamath Proof Explorer

Theorem subfacp1lem5

Description: Lemma for subfacp1 . In subfacp1lem6 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( f1 ) ) = 1 . In this lemma, we show that the subset of all N + 1 derangements with ( f( f1 ) ) =/= 1 for fixed M = ( f1 ) 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 ( f1 ) = 1 and ( fx ) =/= 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)

Ref Expression
Hypotheses 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 subfacp1lem5 
|- ( ph -> ( # ` B ) = ( S ` N ) )

Proof

Step Hyp Ref Expression
1 derang.d 
 |-  D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
2 subfac.n 
 |-  S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
3 subfacp1lem.a 
 |-  A = { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) }
4 subfacp1lem1.n 
 |-  ( ph -> N e. NN )
5 subfacp1lem1.m 
 |-  ( ph -> M e. ( 2 ... ( N + 1 ) ) )
6 subfacp1lem1.x 
 |-  M e. _V
7 subfacp1lem1.k 
 |-  K = ( ( 2 ... ( N + 1 ) ) \ { M } )
8 subfacp1lem5.b 
 |-  B = { g e. A | ( ( g ` 1 ) = M /\ ( g ` M ) =/= 1 ) }
9 subfacp1lem5.f 
 |-  F = ( ( _I |` K ) u. { <. 1 , M >. , <. M , 1 >. } )
10 subfacp1lem5.c 
 |-  C = { f | ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) }
11 fzfi 
 |-  ( 1 ... ( N + 1 ) ) e. Fin
12 deranglem 
 |-  ( ( 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 )
13 11 12 ax-mp 
 |-  { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) } e. Fin
14 3 13 eqeltri 
 |-  A e. Fin
15 8 ssrab3 
 |-  B C_ A
16 ssfi 
 |-  ( ( A e. Fin /\ B C_ A ) -> B e. Fin )
17 14 15 16 mp2an 
 |-  B e. Fin
18 17 elexi 
 |-  B e. _V
19 18 a1i 
 |-  ( ph -> B e. _V )
20 eqid 
 |-  ( b e. B |-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ) = ( b e. B |-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) )
21 f1oi 
 |-  ( _I |` K ) : K -1-1-onto-> K
22 21 a1i 
 |-  ( ph -> ( _I |` K ) : K -1-1-onto-> K )
23 1 2 3 4 5 6 7 9 22 subfacp1lem2a 
 |-  ( ph -> ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( F ` 1 ) = M /\ ( F ` M ) = 1 ) )
24 23 simp1d 
 |-  ( ph -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
25 fveq1 
 |-  ( g = b -> ( g ` 1 ) = ( b ` 1 ) )
26 25 eqeq1d 
 |-  ( g = b -> ( ( g ` 1 ) = M <-> ( b ` 1 ) = M ) )
27 fveq1 
 |-  ( g = b -> ( g ` M ) = ( b ` M ) )
28 27 neeq1d 
 |-  ( g = b -> ( ( g ` M ) =/= 1 <-> ( b ` M ) =/= 1 ) )
29 26 28 anbi12d 
 |-  ( g = b -> ( ( ( g ` 1 ) = M /\ ( g ` M ) =/= 1 ) <-> ( ( b ` 1 ) = M /\ ( b ` M ) =/= 1 ) ) )
30 29 8 elrab2 
 |-  ( b e. B <-> ( b e. A /\ ( ( b ` 1 ) = M /\ ( b ` M ) =/= 1 ) ) )
31 30 bilani 
 |-  ( ( ph /\ b e. B ) -> ( b e. A /\ ( ( b ` 1 ) = M /\ ( b ` M ) =/= 1 ) ) )
32 31 simpld 
 |-  ( ( ph /\ b e. B ) -> b e. A )
33 vex 
 |-  b e. _V
34 f1oeq1 
 |-  ( f = b -> ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) <-> b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
35 fveq1 
 |-  ( f = b -> ( f ` y ) = ( b ` y ) )
36 35 neeq1d 
 |-  ( f = b -> ( ( f ` y ) =/= y <-> ( b ` y ) =/= y ) )
37 36 ralbidv 
 |-  ( f = b -> ( A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y <-> A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y ) )
38 34 37 anbi12d 
 |-  ( 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 ) ) )
39 33 38 3 elab2 
 |-  ( b e. A <-> ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y ) )
40 32 39 sylib 
 |-  ( ( ph /\ b e. B ) -> ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y ) )
41 40 simpld 
 |-  ( ( ph /\ b e. B ) -> b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
42 f1oco 
 |-  ( ( 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 ) ) )
43 24 41 42 syl2an2r 
 |-  ( ( ph /\ b e. B ) -> ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
44 f1of1 
 |-  ( ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) )
45 df-f1 
 |-  ( ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) <-> ( ( F o. b ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ Fun `' ( F o. b ) ) )
46 45 simprbi 
 |-  ( ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) -> Fun `' ( F o. b ) )
47 43 44 46 3syl 
 |-  ( ( ph /\ b e. B ) -> Fun `' ( F o. b ) )
48 f1ofn 
 |-  ( ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( F o. b ) Fn ( 1 ... ( N + 1 ) ) )
49 fnresdm 
 |-  ( ( F o. b ) Fn ( 1 ... ( N + 1 ) ) -> ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) = ( F o. b ) )
50 f1oeq1 
 |-  ( ( ( 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 ) ) ) )
51 43 48 49 50 4syl 
 |-  ( ( 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 ) ) ) )
52 43 51 mpbird 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
53 f1ofo 
 |-  ( ( ( 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 ) ) )
54 52 53 syl 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -onto-> ( 1 ... ( N + 1 ) ) )
55 1ex 
 |-  1 e. _V
56 55 55 f1osn 
 |-  { <. 1 , 1 >. } : { 1 } -1-1-onto-> { 1 }
57 43 48 syl 
 |-  ( ( ph /\ b e. B ) -> ( F o. b ) Fn ( 1 ... ( N + 1 ) ) )
58 4 peano2nnd 
 |-  ( ph -> ( N + 1 ) e. NN )
59 nnuz 
 |-  NN = ( ZZ>= ` 1 )
60 58 59 eleqtrdi 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
61 eluzfz1 
 |-  ( ( N + 1 ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( N + 1 ) ) )
62 60 61 syl 
 |-  ( ph -> 1 e. ( 1 ... ( N + 1 ) ) )
63 62 adantr 
 |-  ( ( ph /\ b e. B ) -> 1 e. ( 1 ... ( N + 1 ) ) )
64 fnressn 
 |-  ( ( ( F o. b ) Fn ( 1 ... ( N + 1 ) ) /\ 1 e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. b ) |` { 1 } ) = { <. 1 , ( ( F o. b ) ` 1 ) >. } )
65 57 63 64 syl2anc 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` { 1 } ) = { <. 1 , ( ( F o. b ) ` 1 ) >. } )
66 f1of 
 |-  ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
67 41 66 syl 
 |-  ( ( ph /\ b e. B ) -> b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
68 67 63 fvco3d 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) ` 1 ) = ( F ` ( b ` 1 ) ) )
69 31 simprd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) = M /\ ( b ` M ) =/= 1 ) )
70 69 simpld 
 |-  ( ( ph /\ b e. B ) -> ( b ` 1 ) = M )
71 70 fveq2d 
 |-  ( ( ph /\ b e. B ) -> ( F ` ( b ` 1 ) ) = ( F ` M ) )
72 23 simp3d 
 |-  ( ph -> ( F ` M ) = 1 )
73 72 adantr 
 |-  ( ( ph /\ b e. B ) -> ( F ` M ) = 1 )
74 68 71 73 3eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) ` 1 ) = 1 )
75 74 opeq2d 
 |-  ( ( ph /\ b e. B ) -> <. 1 , ( ( F o. b ) ` 1 ) >. = <. 1 , 1 >. )
76 75 sneqd 
 |-  ( ( ph /\ b e. B ) -> { <. 1 , ( ( F o. b ) ` 1 ) >. } = { <. 1 , 1 >. } )
77 65 76 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` { 1 } ) = { <. 1 , 1 >. } )
78 77 f1oeq1d 
 |-  ( ( ph /\ b e. B ) -> ( ( ( F o. b ) |` { 1 } ) : { 1 } -1-1-onto-> { 1 } <-> { <. 1 , 1 >. } : { 1 } -1-1-onto-> { 1 } ) )
79 56 78 mpbiri 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` { 1 } ) : { 1 } -1-1-onto-> { 1 } )
80 f1ofo 
 |-  ( ( ( F o. b ) |` { 1 } ) : { 1 } -1-1-onto-> { 1 } -> ( ( F o. b ) |` { 1 } ) : { 1 } -onto-> { 1 } )
81 79 80 syl 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` { 1 } ) : { 1 } -onto-> { 1 } )
82 resdif 
 |-  ( ( 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 } ) )
83 47 54 81 82 syl3anc 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) )
84 fzsplit 
 |-  ( 1 e. ( 1 ... ( N + 1 ) ) -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... ( N + 1 ) ) ) )
85 62 84 syl 
 |-  ( ph -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... ( N + 1 ) ) ) )
86 1z 
 |-  1 e. ZZ
87 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
88 86 87 ax-mp 
 |-  ( 1 ... 1 ) = { 1 }
89 1p1e2 
 |-  ( 1 + 1 ) = 2
90 89 oveq1i 
 |-  ( ( 1 + 1 ) ... ( N + 1 ) ) = ( 2 ... ( N + 1 ) )
91 88 90 uneq12i 
 |-  ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... ( N + 1 ) ) ) = ( { 1 } u. ( 2 ... ( N + 1 ) ) )
92 85 91 eqtr2di 
 |-  ( ph -> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) )
93 62 snssd 
 |-  ( ph -> { 1 } C_ ( 1 ... ( N + 1 ) ) )
94 incom 
 |-  ( { 1 } i^i ( 2 ... ( N + 1 ) ) ) = ( ( 2 ... ( N + 1 ) ) i^i { 1 } )
95 1lt2 
 |-  1 < 2
96 1re 
 |-  1 e. RR
97 2re 
 |-  2 e. RR
98 96 97 ltnlei 
 |-  ( 1 < 2 <-> -. 2 <_ 1 )
99 95 98 mpbi 
 |-  -. 2 <_ 1
100 elfzle1 
 |-  ( 1 e. ( 2 ... ( N + 1 ) ) -> 2 <_ 1 )
101 99 100 mto 
 |-  -. 1 e. ( 2 ... ( N + 1 ) )
102 disjsn 
 |-  ( ( ( 2 ... ( N + 1 ) ) i^i { 1 } ) = (/) <-> -. 1 e. ( 2 ... ( N + 1 ) ) )
103 101 102 mpbir 
 |-  ( ( 2 ... ( N + 1 ) ) i^i { 1 } ) = (/)
104 94 103 eqtri 
 |-  ( { 1 } i^i ( 2 ... ( N + 1 ) ) ) = (/)
105 uneqdifeq 
 |-  ( ( { 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 ) ) ) )
106 93 104 105 sylancl 
 |-  ( ph -> ( ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) <-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) ) )
107 92 106 mpbid 
 |-  ( ph -> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) )
108 107 adantr 
 |-  ( ( ph /\ b e. B ) -> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) )
109 reseq2 
 |-  ( ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) -> ( ( F o. b ) |` ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) )
110 109 f1oeq1d 
 |-  ( ( ( 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 } ) ) )
111 f1oeq2 
 |-  ( ( ( 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 } ) ) )
112 f1oeq3 
 |-  ( ( ( 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 ) ) ) )
113 110 111 112 3bitrd 
 |-  ( ( ( 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 ) ) ) )
114 108 113 syl 
 |-  ( ( 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 ) ) ) )
115 83 114 mpbid 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) )
116 67 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
117 fzp1ss 
 |-  ( 1 e. ZZ -> ( ( 1 + 1 ) ... ( N + 1 ) ) C_ ( 1 ... ( N + 1 ) ) )
118 86 117 ax-mp 
 |-  ( ( 1 + 1 ) ... ( N + 1 ) ) C_ ( 1 ... ( N + 1 ) )
119 90 118 eqsstrri 
 |-  ( 2 ... ( N + 1 ) ) C_ ( 1 ... ( N + 1 ) )
120 simpr 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> y e. ( 2 ... ( N + 1 ) ) )
121 119 120 sselid 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> y e. ( 1 ... ( N + 1 ) ) )
122 116 121 fvco3d 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( F o. b ) ` y ) = ( F ` ( b ` y ) ) )
123 1 2 3 4 5 6 7 8 9 subfacp1lem4 
 |-  ( ph -> `' F = F )
124 123 fveq1d 
 |-  ( ph -> ( `' F ` y ) = ( F ` y ) )
125 124 ad2antrr 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( `' F ` y ) = ( F ` y ) )
126 69 simprd 
 |-  ( ( ph /\ b e. B ) -> ( b ` M ) =/= 1 )
127 126 73 neeqtrrd 
 |-  ( ( ph /\ b e. B ) -> ( b ` M ) =/= ( F ` M ) )
128 127 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( b ` M ) =/= ( F ` M ) )
129 fveq2 
 |-  ( y = M -> ( b ` y ) = ( b ` M ) )
130 fveq2 
 |-  ( y = M -> ( F ` y ) = ( F ` M ) )
131 129 130 neeq12d 
 |-  ( y = M -> ( ( b ` y ) =/= ( F ` y ) <-> ( b ` M ) =/= ( F ` M ) ) )
132 128 131 syl5ibrcom 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( y = M -> ( b ` y ) =/= ( F ` y ) ) )
133 119 sseli 
 |-  ( y e. ( 2 ... ( N + 1 ) ) -> y e. ( 1 ... ( N + 1 ) ) )
134 40 simprd 
 |-  ( ( ph /\ b e. B ) -> A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y )
135 134 r19.21bi 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( b ` y ) =/= y )
136 133 135 sylan2 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( b ` y ) =/= y )
137 136 adantrr 
 |-  ( ( ( ph /\ b e. B ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( b ` y ) =/= y )
138 7 eleq2i 
 |-  ( y e. K <-> y e. ( ( 2 ... ( N + 1 ) ) \ { M } ) )
139 eldifsn 
 |-  ( y e. ( ( 2 ... ( N + 1 ) ) \ { M } ) <-> ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) )
140 138 139 bitri 
 |-  ( y e. K <-> ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) )
141 1 2 3 4 5 6 7 9 22 subfacp1lem2b 
 |-  ( ( ph /\ y e. K ) -> ( F ` y ) = ( ( _I |` K ) ` y ) )
142 fvresi 
 |-  ( y e. K -> ( ( _I |` K ) ` y ) = y )
143 142 adantl 
 |-  ( ( ph /\ y e. K ) -> ( ( _I |` K ) ` y ) = y )
144 141 143 eqtrd 
 |-  ( ( ph /\ y e. K ) -> ( F ` y ) = y )
145 140 144 sylan2br 
 |-  ( ( ph /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( F ` y ) = y )
146 145 adantlr 
 |-  ( ( ( ph /\ b e. B ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( F ` y ) = y )
147 137 146 neeqtrrd 
 |-  ( ( ( ph /\ b e. B ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( b ` y ) =/= ( F ` y ) )
148 147 expr 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( y =/= M -> ( b ` y ) =/= ( F ` y ) ) )
149 132 148 pm2.61dne 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( b ` y ) =/= ( F ` y ) )
150 149 necomd 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( F ` y ) =/= ( b ` y ) )
151 125 150 eqnetrd 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( `' F ` y ) =/= ( b ` y ) )
152 24 adantr 
 |-  ( ( ph /\ b e. B ) -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
153 ffvelcdm 
 |-  ( ( b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( b ` y ) e. ( 1 ... ( N + 1 ) ) )
154 67 133 153 syl2an 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( b ` y ) e. ( 1 ... ( N + 1 ) ) )
155 f1ocnvfv 
 |-  ( ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( b ` y ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( F ` ( b ` y ) ) = y -> ( `' F ` y ) = ( b ` y ) ) )
156 152 154 155 syl2an2r 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( F ` ( b ` y ) ) = y -> ( `' F ` y ) = ( b ` y ) ) )
157 156 necon3d 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( `' F ` y ) =/= ( b ` y ) -> ( F ` ( b ` y ) ) =/= y ) )
158 151 157 mpd 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( F ` ( b ` y ) ) =/= y )
159 122 158 eqnetrd 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( F o. b ) ` y ) =/= y )
160 159 ralrimiva 
 |-  ( ( ph /\ b e. B ) -> A. y e. ( 2 ... ( N + 1 ) ) ( ( F o. b ) ` y ) =/= y )
161 f1of 
 |-  ( ( _I |` K ) : K -1-1-onto-> K -> ( _I |` K ) : K --> K )
162 21 161 ax-mp 
 |-  ( _I |` K ) : K --> K
163 fzfi 
 |-  ( 2 ... ( N + 1 ) ) e. Fin
164 difexg 
 |-  ( ( 2 ... ( N + 1 ) ) e. Fin -> ( ( 2 ... ( N + 1 ) ) \ { M } ) e. _V )
165 163 164 ax-mp 
 |-  ( ( 2 ... ( N + 1 ) ) \ { M } ) e. _V
166 7 165 eqeltri 
 |-  K e. _V
167 fex 
 |-  ( ( ( _I |` K ) : K --> K /\ K e. _V ) -> ( _I |` K ) e. _V )
168 162 166 167 mp2an 
 |-  ( _I |` K ) e. _V
169 prex 
 |-  { <. 1 , M >. , <. M , 1 >. } e. _V
170 168 169 unex 
 |-  ( ( _I |` K ) u. { <. 1 , M >. , <. M , 1 >. } ) e. _V
171 9 170 eqeltri 
 |-  F e. _V
172 171 33 coex 
 |-  ( F o. b ) e. _V
173 172 resex 
 |-  ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) e. _V
174 f1oeq1 
 |-  ( 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 ) ) ) )
175 fveq1 
 |-  ( f = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) -> ( f ` y ) = ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) )
176 fvres 
 |-  ( y e. ( 2 ... ( N + 1 ) ) -> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) = ( ( F o. b ) ` y ) )
177 175 176 sylan9eq 
 |-  ( ( f = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( f ` y ) = ( ( F o. b ) ` y ) )
178 177 neeq1d 
 |-  ( ( f = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( f ` y ) =/= y <-> ( ( F o. b ) ` y ) =/= y ) )
179 178 ralbidva 
 |-  ( 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 ) )
180 174 179 anbi12d 
 |-  ( 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 ) ) )
181 173 180 10 elab2 
 |-  ( ( ( 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 ) )
182 115 160 181 sylanbrc 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) e. C )
183 vex 
 |-  c e. _V
184 f1oeq1 
 |-  ( f = c -> ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) <-> c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) ) )
185 fveq1 
 |-  ( f = c -> ( f ` y ) = ( c ` y ) )
186 185 neeq1d 
 |-  ( f = c -> ( ( f ` y ) =/= y <-> ( c ` y ) =/= y ) )
187 186 ralbidv 
 |-  ( f = c -> ( A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y <-> A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y ) )
188 184 187 anbi12d 
 |-  ( 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 ) ) )
189 183 188 10 elab2 
 |-  ( c e. C <-> ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y ) )
190 189 bilani 
 |-  ( ( ph /\ c e. C ) -> ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y ) )
191 190 simpld 
 |-  ( ( ph /\ c e. C ) -> c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) )
192 f1oun 
 |-  ( ( ( { <. 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 ) ) ) )
193 104 104 192 mpanr12 
 |-  ( ( { <. 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 ) ) ) )
194 56 191 193 sylancr 
 |-  ( ( ph /\ c e. C ) -> ( { <. 1 , 1 >. } u. c ) : ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) )
195 f1oeq2 
 |-  ( ( { 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 ) ) ) ) )
196 f1oeq3 
 |-  ( ( { 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 ) ) ) )
197 195 196 bitrd 
 |-  ( ( { 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 ) ) ) )
198 92 197 syl 
 |-  ( 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 ) ) ) )
199 198 biimpa 
 |-  ( ( 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 ) ) )
200 194 199 syldan 
 |-  ( ( ph /\ c e. C ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
201 f1oco 
 |-  ( ( 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 ) ) )
202 24 200 201 syl2an2r 
 |-  ( ( ph /\ c e. C ) -> ( F o. ( { <. 1 , 1 >. } u. c ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
203 f1of 
 |-  ( ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
204 200 203 syl 
 |-  ( ( ph /\ c e. C ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
205 fvco3 
 |-  ( ( ( { <. 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 ) ) )
206 204 205 sylan 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) = ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
207 124 ad2antrr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( `' F ` y ) = ( F ` y ) )
208 simpr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> y e. ( 1 ... ( N + 1 ) ) )
209 92 ad2antrr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) )
210 208 209 eleqtrrd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> y e. ( { 1 } u. ( 2 ... ( N + 1 ) ) ) )
211 elun 
 |-  ( y e. ( { 1 } u. ( 2 ... ( N + 1 ) ) ) <-> ( y e. { 1 } \/ y e. ( 2 ... ( N + 1 ) ) ) )
212 210 211 sylib 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( y e. { 1 } \/ y e. ( 2 ... ( N + 1 ) ) ) )
213 nelne2 
 |-  ( ( M e. ( 2 ... ( N + 1 ) ) /\ -. 1 e. ( 2 ... ( N + 1 ) ) ) -> M =/= 1 )
214 5 101 213 sylancl 
 |-  ( ph -> M =/= 1 )
215 214 adantr 
 |-  ( ( ph /\ c e. C ) -> M =/= 1 )
216 23 simp2d 
 |-  ( ph -> ( F ` 1 ) = M )
217 216 adantr 
 |-  ( ( ph /\ c e. C ) -> ( F ` 1 ) = M )
218 f1ofun 
 |-  ( ( { <. 1 , 1 >. } u. c ) : ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -> Fun ( { <. 1 , 1 >. } u. c ) )
219 194 218 syl 
 |-  ( ( ph /\ c e. C ) -> Fun ( { <. 1 , 1 >. } u. c ) )
220 ssun1 
 |-  { <. 1 , 1 >. } C_ ( { <. 1 , 1 >. } u. c )
221 55 snid 
 |-  1 e. { 1 }
222 55 dmsnop 
 |-  dom { <. 1 , 1 >. } = { 1 }
223 221 222 eleqtrri 
 |-  1 e. dom { <. 1 , 1 >. }
224 funssfv 
 |-  ( ( 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 ) )
225 220 223 224 mp3an23 
 |-  ( Fun ( { <. 1 , 1 >. } u. c ) -> ( ( { <. 1 , 1 >. } u. c ) ` 1 ) = ( { <. 1 , 1 >. } ` 1 ) )
226 219 225 syl 
 |-  ( ( ph /\ c e. C ) -> ( ( { <. 1 , 1 >. } u. c ) ` 1 ) = ( { <. 1 , 1 >. } ` 1 ) )
227 55 55 fvsn 
 |-  ( { <. 1 , 1 >. } ` 1 ) = 1
228 226 227 eqtrdi 
 |-  ( ( ph /\ c e. C ) -> ( ( { <. 1 , 1 >. } u. c ) ` 1 ) = 1 )
229 215 217 228 3netr4d 
 |-  ( ( ph /\ c e. C ) -> ( F ` 1 ) =/= ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
230 elsni 
 |-  ( y e. { 1 } -> y = 1 )
231 230 fveq2d 
 |-  ( y e. { 1 } -> ( F ` y ) = ( F ` 1 ) )
232 230 fveq2d 
 |-  ( y e. { 1 } -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
233 231 232 neeq12d 
 |-  ( y e. { 1 } -> ( ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> ( F ` 1 ) =/= ( ( { <. 1 , 1 >. } u. c ) ` 1 ) ) )
234 229 233 syl5ibrcom 
 |-  ( ( ph /\ c e. C ) -> ( y e. { 1 } -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
235 234 imp 
 |-  ( ( ( ph /\ c e. C ) /\ y e. { 1 } ) -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
236 219 adantr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> Fun ( { <. 1 , 1 >. } u. c ) )
237 ssun2 
 |-  c C_ ( { <. 1 , 1 >. } u. c )
238 237 a1i 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> c C_ ( { <. 1 , 1 >. } u. c ) )
239 f1odm 
 |-  ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) -> dom c = ( 2 ... ( N + 1 ) ) )
240 191 239 syl 
 |-  ( ( ph /\ c e. C ) -> dom c = ( 2 ... ( N + 1 ) ) )
241 240 eleq2d 
 |-  ( ( ph /\ c e. C ) -> ( y e. dom c <-> y e. ( 2 ... ( N + 1 ) ) ) )
242 241 biimpar 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> y e. dom c )
243 funssfv 
 |-  ( ( Fun ( { <. 1 , 1 >. } u. c ) /\ c C_ ( { <. 1 , 1 >. } u. c ) /\ y e. dom c ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( c ` y ) )
244 236 238 242 243 syl3anc 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( c ` y ) )
245 f1of 
 |-  ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) -> c : ( 2 ... ( N + 1 ) ) --> ( 2 ... ( N + 1 ) ) )
246 191 245 syl 
 |-  ( ( ph /\ c e. C ) -> c : ( 2 ... ( N + 1 ) ) --> ( 2 ... ( N + 1 ) ) )
247 5 adantr 
 |-  ( ( ph /\ c e. C ) -> M e. ( 2 ... ( N + 1 ) ) )
248 246 247 ffvelcdmd 
 |-  ( ( ph /\ c e. C ) -> ( c ` M ) e. ( 2 ... ( N + 1 ) ) )
249 nelne2 
 |-  ( ( ( c ` M ) e. ( 2 ... ( N + 1 ) ) /\ -. 1 e. ( 2 ... ( N + 1 ) ) ) -> ( c ` M ) =/= 1 )
250 248 101 249 sylancl 
 |-  ( ( ph /\ c e. C ) -> ( c ` M ) =/= 1 )
251 250 adantr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( c ` M ) =/= 1 )
252 72 ad2antrr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( F ` M ) = 1 )
253 251 252 neeqtrrd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( c ` M ) =/= ( F ` M ) )
254 fveq2 
 |-  ( y = M -> ( c ` y ) = ( c ` M ) )
255 254 130 neeq12d 
 |-  ( y = M -> ( ( c ` y ) =/= ( F ` y ) <-> ( c ` M ) =/= ( F ` M ) ) )
256 253 255 syl5ibrcom 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( y = M -> ( c ` y ) =/= ( F ` y ) ) )
257 190 simprd 
 |-  ( ( ph /\ c e. C ) -> A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y )
258 257 r19.21bi 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( c ` y ) =/= y )
259 258 adantrr 
 |-  ( ( ( ph /\ c e. C ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( c ` y ) =/= y )
260 145 adantlr 
 |-  ( ( ( ph /\ c e. C ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( F ` y ) = y )
261 259 260 neeqtrrd 
 |-  ( ( ( ph /\ c e. C ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( c ` y ) =/= ( F ` y ) )
262 261 expr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( y =/= M -> ( c ` y ) =/= ( F ` y ) ) )
263 256 262 pm2.61dne 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( c ` y ) =/= ( F ` y ) )
264 244 263 eqnetrd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) =/= ( F ` y ) )
265 264 necomd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
266 235 265 jaodan 
 |-  ( ( ( ph /\ c e. C ) /\ ( y e. { 1 } \/ y e. ( 2 ... ( N + 1 ) ) ) ) -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
267 212 266 syldan 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
268 207 267 eqnetrd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( `' F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
269 24 adantr 
 |-  ( ( ph /\ c e. C ) -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
270 204 ffvelcdmda 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) e. ( 1 ... ( N + 1 ) ) )
271 f1ocnvfv 
 |-  ( ( 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 ) ) )
272 269 270 271 syl2an2r 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) = y -> ( `' F ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
273 272 necon3d 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( `' F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) -> ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) =/= y ) )
274 268 273 mpd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) =/= y )
275 206 274 eqnetrd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) =/= y )
276 275 ralrimiva 
 |-  ( ( ph /\ c e. C ) -> A. y e. ( 1 ... ( N + 1 ) ) ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) =/= y )
277 snex 
 |-  { <. 1 , 1 >. } e. _V
278 277 183 unex 
 |-  ( { <. 1 , 1 >. } u. c ) e. _V
279 171 278 coex 
 |-  ( F o. ( { <. 1 , 1 >. } u. c ) ) e. _V
280 f1oeq1 
 |-  ( 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 ) ) ) )
281 fveq1 
 |-  ( f = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( f ` y ) = ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) )
282 281 neeq1d 
 |-  ( f = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( ( f ` y ) =/= y <-> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) =/= y ) )
283 282 ralbidv 
 |-  ( 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 ) )
284 280 283 anbi12d 
 |-  ( 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 ) ) )
285 279 284 3 elab2 
 |-  ( ( 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 ) )
286 202 276 285 sylanbrc 
 |-  ( ( ph /\ c e. C ) -> ( F o. ( { <. 1 , 1 >. } u. c ) ) e. A )
287 62 adantr 
 |-  ( ( ph /\ c e. C ) -> 1 e. ( 1 ... ( N + 1 ) ) )
288 204 287 fvco3d 
 |-  ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = ( F ` ( ( { <. 1 , 1 >. } u. c ) ` 1 ) ) )
289 228 fveq2d 
 |-  ( ( ph /\ c e. C ) -> ( F ` ( ( { <. 1 , 1 >. } u. c ) ` 1 ) ) = ( F ` 1 ) )
290 288 289 217 3eqtrd 
 |-  ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = M )
291 119 5 sselid 
 |-  ( ph -> M e. ( 1 ... ( N + 1 ) ) )
292 291 adantr 
 |-  ( ( ph /\ c e. C ) -> M e. ( 1 ... ( N + 1 ) ) )
293 204 292 fvco3d 
 |-  ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) = ( F ` ( ( { <. 1 , 1 >. } u. c ) ` M ) ) )
294 237 a1i 
 |-  ( ( ph /\ c e. C ) -> c C_ ( { <. 1 , 1 >. } u. c ) )
295 247 240 eleqtrrd 
 |-  ( ( ph /\ c e. C ) -> M e. dom c )
296 funssfv 
 |-  ( ( Fun ( { <. 1 , 1 >. } u. c ) /\ c C_ ( { <. 1 , 1 >. } u. c ) /\ M e. dom c ) -> ( ( { <. 1 , 1 >. } u. c ) ` M ) = ( c ` M ) )
297 219 294 295 296 syl3anc 
 |-  ( ( ph /\ c e. C ) -> ( ( { <. 1 , 1 >. } u. c ) ` M ) = ( c ` M ) )
298 297 fveq2d 
 |-  ( ( ph /\ c e. C ) -> ( F ` ( ( { <. 1 , 1 >. } u. c ) ` M ) ) = ( F ` ( c ` M ) ) )
299 293 298 eqtrd 
 |-  ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) = ( F ` ( c ` M ) ) )
300 123 fveq1d 
 |-  ( ph -> ( `' F ` 1 ) = ( F ` 1 ) )
301 300 216 eqtrd 
 |-  ( ph -> ( `' F ` 1 ) = M )
302 301 adantr 
 |-  ( ( ph /\ c e. C ) -> ( `' F ` 1 ) = M )
303 id 
 |-  ( y = M -> y = M )
304 254 303 neeq12d 
 |-  ( y = M -> ( ( c ` y ) =/= y <-> ( c ` M ) =/= M ) )
305 304 257 247 rspcdva 
 |-  ( ( ph /\ c e. C ) -> ( c ` M ) =/= M )
306 305 necomd 
 |-  ( ( ph /\ c e. C ) -> M =/= ( c ` M ) )
307 302 306 eqnetrd 
 |-  ( ( ph /\ c e. C ) -> ( `' F ` 1 ) =/= ( c ` M ) )
308 119 248 sselid 
 |-  ( ( ph /\ c e. C ) -> ( c ` M ) e. ( 1 ... ( N + 1 ) ) )
309 f1ocnvfv 
 |-  ( ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( c ` M ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( F ` ( c ` M ) ) = 1 -> ( `' F ` 1 ) = ( c ` M ) ) )
310 24 308 309 syl2an2r 
 |-  ( ( ph /\ c e. C ) -> ( ( F ` ( c ` M ) ) = 1 -> ( `' F ` 1 ) = ( c ` M ) ) )
311 310 necon3d 
 |-  ( ( ph /\ c e. C ) -> ( ( `' F ` 1 ) =/= ( c ` M ) -> ( F ` ( c ` M ) ) =/= 1 ) )
312 307 311 mpd 
 |-  ( ( ph /\ c e. C ) -> ( F ` ( c ` M ) ) =/= 1 )
313 299 312 eqnetrd 
 |-  ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) =/= 1 )
314 290 313 jca 
 |-  ( ( ph /\ c e. C ) -> ( ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = M /\ ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) =/= 1 ) )
315 fveq1 
 |-  ( g = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( g ` 1 ) = ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) )
316 315 eqeq1d 
 |-  ( g = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( ( g ` 1 ) = M <-> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = M ) )
317 fveq1 
 |-  ( g = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( g ` M ) = ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) )
318 317 neeq1d 
 |-  ( g = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( ( g ` M ) =/= 1 <-> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) =/= 1 ) )
319 316 318 anbi12d 
 |-  ( 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 ) ) )
320 319 8 elrab2 
 |-  ( ( 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 ) ) )
321 286 314 320 sylanbrc 
 |-  ( ( ph /\ c e. C ) -> ( F o. ( { <. 1 , 1 >. } u. c ) ) e. B )
322 24 adantr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
323 f1of1 
 |-  ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> F : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) )
324 322 323 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> F : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) )
325 f1of 
 |-  ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> F : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
326 322 325 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> F : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
327 67 adantrr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
328 326 327 fcod 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( F o. b ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
329 204 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
330 cocan1 
 |-  ( ( 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 ) ) )
331 324 328 329 330 syl3anc 
 |-  ( ( 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 ) ) )
332 coass 
 |-  ( ( F o. F ) o. b ) = ( F o. ( F o. b ) )
333 123 coeq1d 
 |-  ( ph -> ( `' F o. F ) = ( F o. F ) )
334 f1ococnv1 
 |-  ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( `' F o. F ) = ( _I |` ( 1 ... ( N + 1 ) ) ) )
335 24 334 syl 
 |-  ( ph -> ( `' F o. F ) = ( _I |` ( 1 ... ( N + 1 ) ) ) )
336 333 335 eqtr3d 
 |-  ( ph -> ( F o. F ) = ( _I |` ( 1 ... ( N + 1 ) ) ) )
337 336 adantr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( F o. F ) = ( _I |` ( 1 ... ( N + 1 ) ) ) )
338 337 coeq1d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. F ) o. b ) = ( ( _I |` ( 1 ... ( N + 1 ) ) ) o. b ) )
339 fcoi2 
 |-  ( b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) -> ( ( _I |` ( 1 ... ( N + 1 ) ) ) o. b ) = b )
340 327 339 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( _I |` ( 1 ... ( N + 1 ) ) ) o. b ) = b )
341 338 340 eqtrd 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. F ) o. b ) = b )
342 332 341 eqtr3id 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( F o. ( F o. b ) ) = b )
343 342 eqeq1d 
 |-  ( ( 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 ) ) ) )
344 74 adantrr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) ` 1 ) = 1 )
345 228 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` 1 ) = 1 )
346 344 345 eqtr4d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) ` 1 ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
347 fveq2 
 |-  ( y = 1 -> ( ( F o. b ) ` y ) = ( ( F o. b ) ` 1 ) )
348 fveq2 
 |-  ( y = 1 -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
349 347 348 eqeq12d 
 |-  ( y = 1 -> ( ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> ( ( F o. b ) ` 1 ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) ) )
350 55 349 ralsn 
 |-  ( A. y e. { 1 } ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> ( ( F o. b ) ` 1 ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
351 346 350 sylibr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> A. y e. { 1 } ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) )
352 351 biantrurd 
 |-  ( ( 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 ) ) ) )
353 ralunb 
 |-  ( 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 ) ) )
354 352 353 bitr4di 
 |-  ( ( 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 ) ) )
355 176 adantl 
 |-  ( ( ( ph /\ ( b e. B /\ c e. C ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) = ( ( F o. b ) ` y ) )
356 355 eqcomd 
 |-  ( ( ( ph /\ ( b e. B /\ c e. C ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( F o. b ) ` y ) = ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) )
357 244 adantlrl 
 |-  ( ( ( ph /\ ( b e. B /\ c e. C ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( c ` y ) )
358 356 357 eqeq12d 
 |-  ( ( ( 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 ) ) )
359 358 ralbidva 
 |-  ( ( 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 ) ) )
360 92 adantr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) )
361 360 raleqdv 
 |-  ( ( 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 ) ) )
362 354 359 361 3bitr3rd 
 |-  ( ( 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 ) ) )
363 57 adantrr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( F o. b ) Fn ( 1 ... ( N + 1 ) ) )
364 200 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
365 f1ofn 
 |-  ( ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( { <. 1 , 1 >. } u. c ) Fn ( 1 ... ( N + 1 ) ) )
366 364 365 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( { <. 1 , 1 >. } u. c ) Fn ( 1 ... ( N + 1 ) ) )
367 eqfnfv 
 |-  ( ( ( 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 ) ) )
368 363 366 367 syl2anc 
 |-  ( ( 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 ) ) )
369 fnssres 
 |-  ( ( ( F o. b ) Fn ( 1 ... ( N + 1 ) ) /\ ( 2 ... ( N + 1 ) ) C_ ( 1 ... ( N + 1 ) ) ) -> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) Fn ( 2 ... ( N + 1 ) ) )
370 363 119 369 sylancl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) Fn ( 2 ... ( N + 1 ) ) )
371 191 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) )
372 f1ofn 
 |-  ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) -> c Fn ( 2 ... ( N + 1 ) ) )
373 371 372 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> c Fn ( 2 ... ( N + 1 ) ) )
374 eqfnfv 
 |-  ( ( ( ( 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 ) ) )
375 370 373 374 syl2anc 
 |-  ( ( 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 ) ) )
376 362 368 375 3bitr4d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) = ( { <. 1 , 1 >. } u. c ) <-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) = c ) )
377 eqcom 
 |-  ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) = c <-> c = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) )
378 376 377 bitrdi 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) = ( { <. 1 , 1 >. } u. c ) <-> c = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ) )
379 331 343 378 3bitr3d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b = ( F o. ( { <. 1 , 1 >. } u. c ) ) <-> c = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ) )
380 20 182 321 379 f1o2d 
 |-  ( ph -> ( b e. B |-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ) : B -1-1-onto-> C )
381 19 380 hasheqf1od 
 |-  ( ph -> ( # ` B ) = ( # ` C ) )
382 1 2 derangen2 
 |-  ( ( 2 ... ( N + 1 ) ) e. Fin -> ( D ` ( 2 ... ( N + 1 ) ) ) = ( S ` ( # ` ( 2 ... ( N + 1 ) ) ) ) )
383 1 derangval 
 |-  ( ( 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 ) } ) )
384 10 fveq2i 
 |-  ( # ` C ) = ( # ` { f | ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) } )
385 383 384 eqtr4di 
 |-  ( ( 2 ... ( N + 1 ) ) e. Fin -> ( D ` ( 2 ... ( N + 1 ) ) ) = ( # ` C ) )
386 382 385 eqtr3d 
 |-  ( ( 2 ... ( N + 1 ) ) e. Fin -> ( S ` ( # ` ( 2 ... ( N + 1 ) ) ) ) = ( # ` C ) )
387 163 386 ax-mp 
 |-  ( S ` ( # ` ( 2 ... ( N + 1 ) ) ) ) = ( # ` C )
388 4 59 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
389 eluzp1p1 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( N + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
390 388 389 syl 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
391 df-2 
 |-  2 = ( 1 + 1 )
392 391 fveq2i 
 |-  ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
393 390 392 eleqtrrdi 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` 2 ) )
394 hashfz 
 |-  ( ( N + 1 ) e. ( ZZ>= ` 2 ) -> ( # ` ( 2 ... ( N + 1 ) ) ) = ( ( ( N + 1 ) - 2 ) + 1 ) )
395 393 394 syl 
 |-  ( ph -> ( # ` ( 2 ... ( N + 1 ) ) ) = ( ( ( N + 1 ) - 2 ) + 1 ) )
396 58 nncnd 
 |-  ( ph -> ( N + 1 ) e. CC )
397 2cnd 
 |-  ( ph -> 2 e. CC )
398 1cnd 
 |-  ( ph -> 1 e. CC )
399 396 397 398 subsubd 
 |-  ( ph -> ( ( N + 1 ) - ( 2 - 1 ) ) = ( ( ( N + 1 ) - 2 ) + 1 ) )
400 2m1e1 
 |-  ( 2 - 1 ) = 1
401 400 oveq2i 
 |-  ( ( N + 1 ) - ( 2 - 1 ) ) = ( ( N + 1 ) - 1 )
402 4 nncnd 
 |-  ( ph -> N e. CC )
403 ax-1cn 
 |-  1 e. CC
404 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
405 402 403 404 sylancl 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
406 401 405 eqtrid 
 |-  ( ph -> ( ( N + 1 ) - ( 2 - 1 ) ) = N )
407 395 399 406 3eqtr2d 
 |-  ( ph -> ( # ` ( 2 ... ( N + 1 ) ) ) = N )
408 407 fveq2d 
 |-  ( ph -> ( S ` ( # ` ( 2 ... ( N + 1 ) ) ) ) = ( S ` N ) )
409 387 408 eqtr3id 
 |-  ( ph -> ( # ` C ) = ( S ` N ) )
410 381 409 eqtrd 
 |-  ( ph -> ( # ` B ) = ( S ` N ) )