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 = ( SymGrp ` A )
	symgbas.2	|- B = ( Base ` G )
Assertion	symgbasf	|- ( F e. B -> F : A --> A )

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	|- G = ( SymGrp ` A )
2		symgbas.2	|- B = ( Base ` G )
3	1 2	symgbasf1o	|- ( F e. B -> F : A -1-1-onto-> A )
4		f1of	|- ( F : A -1-1-onto-> A -> F : A --> A )
5	3 4	syl	|- ( F e. B -> F : A --> A )