Theorem symgbasf1o

Description: Elements in the symmetric group are 1-1 onto functions. (Contributed by SO, 9-Jul-2018)

	Ref	Expression
Hypotheses	symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symgbas.2	$$⊢B={\mathrm{Base}}_G$$
Assertion	symgbasf1o	$$⊢F\in B\to F:A\underset{1-1\; onto}{⟶}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	elsymgbas2	$$⊢F\in B\to \left(F\in B\leftrightarrow F:A\underset{1-1\; onto}{⟶}A\right)$$
4	3	ibi	$$⊢F\in B\to F:A\underset{1-1\; onto}{⟶}A$$