Metamath Proof Explorer

Theorem subfacp1lem4

Description: Lemma for subfacp1 . The function F , which swaps 1 with M and leaves all other elements alone, is a bijection of order 2 , i.e. it is its own inverse. (Contributed by Mario Carneiro, 19-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 >. } )
Assertion subfacp1lem4 
|- ( ph -> `' F = F )

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 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 ffvelcdmda 
 |-  ( ( 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 )