Description: The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a function. (Contributed by AV, 4-Jan-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | symgfixf.p | ||
symgfixf.q | |||
symgfixf.s | |||
symgfixf.h | |||
Assertion | symgfixf |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | symgfixf.p | ||
2 | symgfixf.q | ||
3 | symgfixf.s | ||
4 | symgfixf.h | ||
5 | eqid | ||
6 | 1 2 3 5 | symgfixelsi | |
7 | 6 4 | fmptd |