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