Theorem symgextsymg

Description: The extension of a permutation is an element of the extended symmetric group. (Contributed by AV, 9-Mar-2019)

	Ref	Expression
Hypotheses	symgext.s	|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
	symgext.e	|- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )
Assertion	symgextsymg	|- ( ( N e. V /\ K e. N /\ Z e. S ) -> E e. ( Base ` ( SymGrp ` 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	1 2	symgextf1o	|- ( ( K e. N /\ Z e. S ) -> E : N -1-1-onto-> N )
4	3	3adant1	|- ( ( N e. V /\ K e. N /\ Z e. S ) -> E : N -1-1-onto-> N )
5		eqid	|- ( SymGrp ` N ) = ( SymGrp ` N )
6		eqid	|- ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
7	5 6	elsymgbas	|- ( N e. V -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
8	7	3ad2ant1	|- ( ( N e. V /\ K e. N /\ Z e. S ) -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
9	4 8	mpbird	|- ( ( N e. V /\ K e. N /\ Z e. S ) -> E e. ( Base ` ( SymGrp ` N ) ) )