Metamath Proof Explorer


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 N if x = K K Z x
Assertion symgextf K N Z S E : N 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 simplll K N Z S x N x = K K N
4 simpllr K N Z S x N ¬ x = K Z S
5 simpr K N Z S x N x N
6 neqne ¬ x = K x K
7 5 6 anim12i K N Z S x N ¬ x = K x N x K
8 eldifsn x N K x N x K
9 7 8 sylibr K N Z S x N ¬ x = K x N K
10 eqid SymGrp N K = SymGrp N K
11 10 1 symgfv Z S x N K Z x N K
12 4 9 11 syl2anc K N Z S x N ¬ x = K Z x N K
13 12 eldifad K N Z S x N ¬ x = K Z x N
14 3 13 ifclda K N Z S x N if x = K K Z x N
15 14 2 fmptd K N Z S E : N N