Metamath Proof Explorer


Theorem symgmov2

Description: For a permutation of a set, each element of the set is replaced by an(other) element of the set. (Contributed by AV, 2-Jan-2019)

Ref Expression
Hypothesis symgmov1.p P = Base SymGrp N
Assertion symgmov2 Q P n N k N Q k = n

Proof

Step Hyp Ref Expression
1 symgmov1.p P = Base SymGrp N
2 eqid SymGrp N = SymGrp N
3 2 1 symgbasf1o Q P Q : N 1-1 onto N
4 f1ofo Q : N 1-1 onto N Q : N onto N
5 foelrni Q : N onto N n N k N Q k = n
6 5 ralrimiva Q : N onto N n N k N Q k = n
7 3 4 6 3syl Q P n N k N Q k = n