Theorem symgbasex

Description: The base set of the symmetric group over a set A exists. (Contributed by AV, 30-Mar-2024)

	Ref	Expression
Hypotheses	symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symgbas.2	$$⊢B={\mathrm{Base}}_G$$
Assertion	symgbasex	$$⊢A\in V\to B\in \mathrm{V}$$

Proof

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