Theorem elsymgbas2

Description: Two ways of saying a function is a 1-1-onto mapping of A to itself. (Contributed by Mario Carneiro, 28-Jan-2015)

	Ref	Expression
Hypotheses	symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symgbas.2	$$⊢B={\mathrm{Base}}_G$$
Assertion	elsymgbas2	$$⊢F\in V\to \left(F\in B\leftrightarrow F:A\underset{1-1\; onto}{⟶}A\right)$$

Proof

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