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 |
|
f1oi |
|- ( _I |` K ) : K -1-1-onto-> K |
11 |
10
|
a1i |
|- ( ph -> ( _I |` K ) : K -1-1-onto-> K ) |
12 |
1 2 3 4 5 6 7 9 11
|
subfacp1lem2a |
|- ( ph -> ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( F ` 1 ) = M /\ ( F ` M ) = 1 ) ) |
13 |
12
|
simp1d |
|- ( ph -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) |
14 |
|
f1ocnv |
|- ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> `' F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) |
15 |
|
f1ofn |
|- ( `' F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> `' F Fn ( 1 ... ( N + 1 ) ) ) |
16 |
13 14 15
|
3syl |
|- ( ph -> `' F Fn ( 1 ... ( N + 1 ) ) ) |
17 |
|
f1ofn |
|- ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> F Fn ( 1 ... ( N + 1 ) ) ) |
18 |
13 17
|
syl |
|- ( ph -> F Fn ( 1 ... ( N + 1 ) ) ) |
19 |
1 2 3 4 5 6 7
|
subfacp1lem1 |
|- ( ph -> ( ( K i^i { 1 , M } ) = (/) /\ ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) /\ ( # ` K ) = ( N - 1 ) ) ) |
20 |
19
|
simp2d |
|- ( ph -> ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) ) |
21 |
20
|
eleq2d |
|- ( ph -> ( x e. ( K u. { 1 , M } ) <-> x e. ( 1 ... ( N + 1 ) ) ) ) |
22 |
21
|
biimpar |
|- ( ( ph /\ x e. ( 1 ... ( N + 1 ) ) ) -> x e. ( K u. { 1 , M } ) ) |
23 |
|
elun |
|- ( x e. ( K u. { 1 , M } ) <-> ( x e. K \/ x e. { 1 , M } ) ) |
24 |
22 23
|
sylib |
|- ( ( ph /\ x e. ( 1 ... ( N + 1 ) ) ) -> ( x e. K \/ x e. { 1 , M } ) ) |
25 |
1 2 3 4 5 6 7 9 11
|
subfacp1lem2b |
|- ( ( ph /\ x e. K ) -> ( F ` x ) = ( ( _I |` K ) ` x ) ) |
26 |
|
fvresi |
|- ( x e. K -> ( ( _I |` K ) ` x ) = x ) |
27 |
26
|
adantl |
|- ( ( ph /\ x e. K ) -> ( ( _I |` K ) ` x ) = x ) |
28 |
25 27
|
eqtrd |
|- ( ( ph /\ x e. K ) -> ( F ` x ) = x ) |
29 |
28
|
fveq2d |
|- ( ( ph /\ x e. K ) -> ( F ` ( F ` x ) ) = ( F ` x ) ) |
30 |
29 28
|
eqtrd |
|- ( ( ph /\ x e. K ) -> ( F ` ( F ` x ) ) = x ) |
31 |
|
vex |
|- x e. _V |
32 |
31
|
elpr |
|- ( x e. { 1 , M } <-> ( x = 1 \/ x = M ) ) |
33 |
12
|
simp2d |
|- ( ph -> ( F ` 1 ) = M ) |
34 |
33
|
fveq2d |
|- ( ph -> ( F ` ( F ` 1 ) ) = ( F ` M ) ) |
35 |
12
|
simp3d |
|- ( ph -> ( F ` M ) = 1 ) |
36 |
34 35
|
eqtrd |
|- ( ph -> ( F ` ( F ` 1 ) ) = 1 ) |
37 |
|
2fveq3 |
|- ( x = 1 -> ( F ` ( F ` x ) ) = ( F ` ( F ` 1 ) ) ) |
38 |
|
id |
|- ( x = 1 -> x = 1 ) |
39 |
37 38
|
eqeq12d |
|- ( x = 1 -> ( ( F ` ( F ` x ) ) = x <-> ( F ` ( F ` 1 ) ) = 1 ) ) |
40 |
36 39
|
syl5ibrcom |
|- ( ph -> ( x = 1 -> ( F ` ( F ` x ) ) = x ) ) |
41 |
35
|
fveq2d |
|- ( ph -> ( F ` ( F ` M ) ) = ( F ` 1 ) ) |
42 |
41 33
|
eqtrd |
|- ( ph -> ( F ` ( F ` M ) ) = M ) |
43 |
|
2fveq3 |
|- ( x = M -> ( F ` ( F ` x ) ) = ( F ` ( F ` M ) ) ) |
44 |
|
id |
|- ( x = M -> x = M ) |
45 |
43 44
|
eqeq12d |
|- ( x = M -> ( ( F ` ( F ` x ) ) = x <-> ( F ` ( F ` M ) ) = M ) ) |
46 |
42 45
|
syl5ibrcom |
|- ( ph -> ( x = M -> ( F ` ( F ` x ) ) = x ) ) |
47 |
40 46
|
jaod |
|- ( ph -> ( ( x = 1 \/ x = M ) -> ( F ` ( F ` x ) ) = x ) ) |
48 |
47
|
imp |
|- ( ( ph /\ ( x = 1 \/ x = M ) ) -> ( F ` ( F ` x ) ) = x ) |
49 |
32 48
|
sylan2b |
|- ( ( ph /\ x e. { 1 , M } ) -> ( F ` ( F ` x ) ) = x ) |
50 |
30 49
|
jaodan |
|- ( ( ph /\ ( x e. K \/ x e. { 1 , M } ) ) -> ( F ` ( F ` x ) ) = x ) |
51 |
24 50
|
syldan |
|- ( ( ph /\ x e. ( 1 ... ( N + 1 ) ) ) -> ( F ` ( F ` x ) ) = x ) |
52 |
13
|
adantr |
|- ( ( ph /\ x e. ( 1 ... ( N + 1 ) ) ) -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) |
53 |
|
f1of |
|- ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> F : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) ) |
54 |
13 53
|
syl |
|- ( ph -> F : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) ) |
55 |
54
|
ffvelrnda |
|- ( ( ph /\ x e. ( 1 ... ( N + 1 ) ) ) -> ( F ` x ) e. ( 1 ... ( N + 1 ) ) ) |
56 |
|
f1ocnvfv |
|- ( ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( F ` x ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( F ` ( F ` x ) ) = x -> ( `' F ` x ) = ( F ` x ) ) ) |
57 |
52 55 56
|
syl2anc |
|- ( ( ph /\ x e. ( 1 ... ( N + 1 ) ) ) -> ( ( F ` ( F ` x ) ) = x -> ( `' F ` x ) = ( F ` x ) ) ) |
58 |
51 57
|
mpd |
|- ( ( ph /\ x e. ( 1 ... ( N + 1 ) ) ) -> ( `' F ` x ) = ( F ` x ) ) |
59 |
16 18 58
|
eqfnfvd |
|- ( ph -> `' F = F ) |