Theorem symgbasfi

Description: The symmetric group on a finite index set is finite. (Contributed by SO, 9-Jul-2018)

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

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgbas.2	$$⊢B={\mathrm{Base}}_G$$
3		mapfi	$$⊢\left(A\in \mathrm{Fin}\wedge A\in \mathrm{Fin}\right)\to A^A\in \mathrm{Fin}$$
4	3	anidms	$$⊢A\in \mathrm{Fin}\to A^A\in \mathrm{Fin}$$
5	1 2	symgbas	$$⊢B=\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
6		f1of	$$⊢f:A\underset{1-1\; onto}{⟶}A\to f:A⟶A$$
7	6	ss2abi	$$⊢\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\subseteq \left\{f|f:A⟶A\right\}$$
8	5 7	eqsstri	$$⊢B\subseteq \left\{f|f:A⟶A\right\}$$
9		mapvalg	$$⊢\left(A\in \mathrm{Fin}\wedge A\in \mathrm{Fin}\right)\to A^A=\left\{f|f:A⟶A\right\}$$
10	9	anidms	$$⊢A\in \mathrm{Fin}\to A^A=\left\{f|f:A⟶A\right\}$$
11	8 10	sseqtrrid	$$⊢A\in \mathrm{Fin}\to B\subseteq A^A$$
12	4 11	ssfid	$$⊢A\in \mathrm{Fin}\to B\in \mathrm{Fin}$$