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=\mathrm{SymGrp}\left(A\right)$$
	symgbas.2	$$⊢B={\mathrm{Base}}_G$$
Assertion	symgbasf	$$⊢F\in B\to F:A⟶A$$

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgbas.2	$$⊢B={\mathrm{Base}}_G$$
3	1 2	symgbasf1o	$$⊢F\in B\to F:A\underset{1-1\; onto}{⟶}A$$
4		f1of	$$⊢F:A\underset{1-1\; onto}{⟶}A\to F:A⟶A$$
5	3 4	syl	$$⊢F\in B\to F:A⟶A$$