symgbasfi

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

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

Metamath Proof Explorer