Theorem subfacp1lem2b

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	subfacp1lem2b	|- ( ( ph /\ X e. K ) -> ( F ` X ) = ( G ` X ) )

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	1 2 3 4 5 6 7 8 9	subfacp1lem2a	|- ( ph -> ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( F ` 1 ) = M /\ ( F ` M ) = 1 ) )
11	10	simp1d	|- ( ph -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
12		f1ofun	|- ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> Fun F )
13	11 12	syl	|- ( ph -> Fun F )
14	13	adantr	|- ( ( ph /\ X e. K ) -> Fun F )
15		ssun1	|- G C_ ( G u. { <. 1 , M >. , <. M , 1 >. } )
16	15 8	sseqtrri	|- G C_ F
17	16	a1i	|- ( ( ph /\ X e. K ) -> G C_ F )
18		f1odm	|- ( G : K -1-1-onto-> K -> dom G = K )
19	9 18	syl	|- ( ph -> dom G = K )
20	19	eleq2d	|- ( ph -> ( X e. dom G <-> X e. K ) )
21	20	biimpar	|- ( ( ph /\ X e. K ) -> X e. dom G )
22		funssfv	|- ( ( Fun F /\ G C_ F /\ X e. dom G ) -> ( F ` X ) = ( G ` X ) )
23	14 17 21 22	syl3anc	|- ( ( ph /\ X e. K ) -> ( F ` X ) = ( G ` X ) )