Theorem symgextf

Description: The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019)

	Ref	Expression
Hypotheses	symgext.s	|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
	symgext.e	|- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )
Assertion	symgextf	|- ( ( K e. N /\ Z e. S ) -> E : N --> N )

Proof

Step	Hyp	Ref	Expression
1		symgext.s	|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
2		symgext.e	|- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )
3		simplll	|- ( ( ( ( K e. N /\ Z e. S ) /\ x e. N ) /\ x = K ) -> K e. N )
4		simpllr	|- ( ( ( ( K e. N /\ Z e. S ) /\ x e. N ) /\ -. x = K ) -> Z e. S )
5		simpr	|- ( ( ( K e. N /\ Z e. S ) /\ x e. N ) -> x e. N )
6		neqne	|- ( -. x = K -> x =/= K )
7	5 6	anim12i	|- ( ( ( ( K e. N /\ Z e. S ) /\ x e. N ) /\ -. x = K ) -> ( x e. N /\ x =/= K ) )
8		eldifsn	|- ( x e. ( N \ { K } ) <-> ( x e. N /\ x =/= K ) )
9	7 8	sylibr	|- ( ( ( ( K e. N /\ Z e. S ) /\ x e. N ) /\ -. x = K ) -> x e. ( N \ { K } ) )
10		eqid	|- ( SymGrp ` ( N \ { K } ) ) = ( SymGrp ` ( N \ { K } ) )
11	10 1	symgfv	|- ( ( Z e. S /\ x e. ( N \ { K } ) ) -> ( Z ` x ) e. ( N \ { K } ) )
12	4 9 11	syl2anc	|- ( ( ( ( K e. N /\ Z e. S ) /\ x e. N ) /\ -. x = K ) -> ( Z ` x ) e. ( N \ { K } ) )
13	12	eldifad	|- ( ( ( ( K e. N /\ Z e. S ) /\ x e. N ) /\ -. x = K ) -> ( Z ` x ) e. N )
14	3 13	ifclda	|- ( ( ( K e. N /\ Z e. S ) /\ x e. N ) -> if ( x = K , K , ( Z ` x ) ) e. N )
15	14 2	fmptd	|- ( ( K e. N /\ Z e. S ) -> E : N --> N )