Metamath Proof Explorer

Theorem subfacp1lem2a

Description: Lemma for subfacp1 . Properties of a bijection on K augmented with the two-element flip to get a bijection on K u. { 1 , M } . (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 } )
subfacp1lem2.5 
|- F = ( G u. { <. 1 , M >. , <. M , 1 >. } )
subfacp1lem2.6 
|- ( ph -> G : K -1-1-onto-> K )
Assertion subfacp1lem2a 
|- ( ph -> ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( F ` 1 ) = M /\ ( F ` M ) = 1 ) )

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 subfacp1lem2.5 
 |-  F = ( G u. { <. 1 , M >. , <. M , 1 >. } )
9 subfacp1lem2.6 
 |-  ( ph -> G : K -1-1-onto-> K )
10 1z 
 |-  1 e. ZZ
11 f1oprswap 
 |-  ( ( 1 e. ZZ /\ M e. _V ) -> { <. 1 , M >. , <. M , 1 >. } : { 1 , M } -1-1-onto-> { 1 , M } )
12 10 6 11 mp2an 
 |-  { <. 1 , M >. , <. M , 1 >. } : { 1 , M } -1-1-onto-> { 1 , M }
13 12 a1i 
 |-  ( ph -> { <. 1 , M >. , <. M , 1 >. } : { 1 , M } -1-1-onto-> { 1 , M } )
14 1 2 3 4 5 6 7 subfacp1lem1 
 |-  ( ph -> ( ( K i^i { 1 , M } ) = (/) /\ ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) /\ ( # ` K ) = ( N - 1 ) ) )
15 14 simp1d 
 |-  ( ph -> ( K i^i { 1 , M } ) = (/) )
16 f1oun 
 |-  ( ( ( G : K -1-1-onto-> K /\ { <. 1 , M >. , <. M , 1 >. } : { 1 , M } -1-1-onto-> { 1 , M } ) /\ ( ( K i^i { 1 , M } ) = (/) /\ ( K i^i { 1 , M } ) = (/) ) ) -> ( G u. { <. 1 , M >. , <. M , 1 >. } ) : ( K u. { 1 , M } ) -1-1-onto-> ( K u. { 1 , M } ) )
17 9 13 15 15 16 syl22anc 
 |-  ( ph -> ( G u. { <. 1 , M >. , <. M , 1 >. } ) : ( K u. { 1 , M } ) -1-1-onto-> ( K u. { 1 , M } ) )
18 14 simp2d 
 |-  ( ph -> ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) )
19 f1oeq1 
 |-  ( F = ( G u. { <. 1 , M >. , <. M , 1 >. } ) -> ( F : ( K u. { 1 , M } ) -1-1-onto-> ( K u. { 1 , M } ) <-> ( G u. { <. 1 , M >. , <. M , 1 >. } ) : ( K u. { 1 , M } ) -1-1-onto-> ( K u. { 1 , M } ) ) )
20 8 19 ax-mp 
 |-  ( F : ( K u. { 1 , M } ) -1-1-onto-> ( K u. { 1 , M } ) <-> ( G u. { <. 1 , M >. , <. M , 1 >. } ) : ( K u. { 1 , M } ) -1-1-onto-> ( K u. { 1 , M } ) )
21 f1oeq2 
 |-  ( ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) -> ( F : ( K u. { 1 , M } ) -1-1-onto-> ( K u. { 1 , M } ) <-> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( K u. { 1 , M } ) ) )
22 20 21 bitr3id 
 |-  ( ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) -> ( ( G u. { <. 1 , M >. , <. M , 1 >. } ) : ( K u. { 1 , M } ) -1-1-onto-> ( K u. { 1 , M } ) <-> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( K u. { 1 , M } ) ) )
23 f1oeq3 
 |-  ( ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) -> ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( K u. { 1 , M } ) <-> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
24 22 23 bitrd 
 |-  ( ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) -> ( ( G u. { <. 1 , M >. , <. M , 1 >. } ) : ( K u. { 1 , M } ) -1-1-onto-> ( K u. { 1 , M } ) <-> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
25 18 24 syl 
 |-  ( ph -> ( ( G u. { <. 1 , M >. , <. M , 1 >. } ) : ( K u. { 1 , M } ) -1-1-onto-> ( K u. { 1 , M } ) <-> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
26 17 25 mpbid 
 |-  ( ph -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
27 f1ofun 
 |-  ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> Fun F )
28 26 27 syl 
 |-  ( ph -> Fun F )
29 snsspr1 
 |-  { <. 1 , M >. } C_ { <. 1 , M >. , <. M , 1 >. }
30 ssun2 
 |-  { <. 1 , M >. , <. M , 1 >. } C_ ( G u. { <. 1 , M >. , <. M , 1 >. } )
31 30 8 sseqtrri 
 |-  { <. 1 , M >. , <. M , 1 >. } C_ F
32 29 31 sstri 
 |-  { <. 1 , M >. } C_ F
33 1ex 
 |-  1 e. _V
34 33 snid 
 |-  1 e. { 1 }
35 6 dmsnop 
 |-  dom { <. 1 , M >. } = { 1 }
36 34 35 eleqtrri 
 |-  1 e. dom { <. 1 , M >. }
37 funssfv 
 |-  ( ( Fun F /\ { <. 1 , M >. } C_ F /\ 1 e. dom { <. 1 , M >. } ) -> ( F ` 1 ) = ( { <. 1 , M >. } ` 1 ) )
38 32 36 37 mp3an23 
 |-  ( Fun F -> ( F ` 1 ) = ( { <. 1 , M >. } ` 1 ) )
39 28 38 syl 
 |-  ( ph -> ( F ` 1 ) = ( { <. 1 , M >. } ` 1 ) )
40 33 6 fvsn 
 |-  ( { <. 1 , M >. } ` 1 ) = M
41 39 40 eqtrdi 
 |-  ( ph -> ( F ` 1 ) = M )
42 snsspr2 
 |-  { <. M , 1 >. } C_ { <. 1 , M >. , <. M , 1 >. }
43 42 31 sstri 
 |-  { <. M , 1 >. } C_ F
44 6 snid 
 |-  M e. { M }
45 33 dmsnop 
 |-  dom { <. M , 1 >. } = { M }
46 44 45 eleqtrri 
 |-  M e. dom { <. M , 1 >. }
47 funssfv 
 |-  ( ( Fun F /\ { <. M , 1 >. } C_ F /\ M e. dom { <. M , 1 >. } ) -> ( F ` M ) = ( { <. M , 1 >. } ` M ) )
48 43 46 47 mp3an23 
 |-  ( Fun F -> ( F ` M ) = ( { <. M , 1 >. } ` M ) )
49 28 48 syl 
 |-  ( ph -> ( F ` M ) = ( { <. M , 1 >. } ` M ) )
50 6 33 fvsn 
 |-  ( { <. M , 1 >. } ` M ) = 1
51 49 50 eqtrdi 
 |-  ( ph -> ( F ` M ) = 1 )
52 26 41 51 3jca 
 |-  ( ph -> ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( F ` 1 ) = M /\ ( F ` M ) = 1 ) )