Metamath Proof Explorer


Theorem symgbasf

Description: A permutation (element of the symmetric group) is a function from a set into itself. (Contributed by AV, 1-Jan-2019)

Ref Expression
Hypotheses symgbas.1 G=SymGrpA
symgbas.2 B=BaseG
Assertion symgbasf FBF:AA

Proof

Step Hyp Ref Expression
1 symgbas.1 G=SymGrpA
2 symgbas.2 B=BaseG
3 1 2 symgbasf1o FBF:A1-1 ontoA
4 f1of F:A1-1 ontoAF:AA
5 3 4 syl FBF:AA