Metamath Proof Explorer


Theorem symgextf1o

Description: The extension of a permutation, fixing the additional element, is a bijection. (Contributed by AV, 7-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 symgextf1o
|- ( ( K e. N /\ Z e. S ) -> E : N -1-1-onto-> 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 symgextf1
 |-  ( ( K e. N /\ Z e. S ) -> E : N -1-1-> N )
4 1 2 symgextfo
 |-  ( ( K e. N /\ Z e. S ) -> E : N -onto-> N )
5 df-f1o
 |-  ( E : N -1-1-onto-> N <-> ( E : N -1-1-> N /\ E : N -onto-> N ) )
6 3 4 5 sylanbrc
 |-  ( ( K e. N /\ Z e. S ) -> E : N -1-1-onto-> N )