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 N if x = K K Z x
Assertion symgextf1o K N Z 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 N if x = K K Z x
3 1 2 symgextf1 K N Z S E : N 1-1 N
4 1 2 symgextfo K N Z 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 N Z S E : N 1-1 onto N