Theorem symg1hash

Description: The symmetric group on a singleton has cardinality 1 . (Contributed by AV, 9-Dec-2018)

	Ref	Expression
Hypotheses	symg1bas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symg1bas.2	$$⊢B={\mathrm{Base}}_G$$
	symg1bas.0	$$⊢A=\left\{I\right\}$$
Assertion	symg1hash	$$⊢I\in V\to \left|B\right|=1$$

Proof

Step	Hyp	Ref	Expression
1		symg1bas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symg1bas.2	$$⊢B={\mathrm{Base}}_G$$
3		symg1bas.0	$$⊢A=\left\{I\right\}$$
4		snfi	$$⊢\left\{I\right\}\in \mathrm{Fin}$$
5	3 4	eqeltri	$$⊢A\in \mathrm{Fin}$$
6	1 2	symghash	$$⊢A\in \mathrm{Fin}\to \left|B\right|=\left|A\right|!$$
7	5 6	ax-mp	$$⊢\left|B\right|=\left|A\right|!$$
8	3	fveq2i	$$⊢\left|A\right|=\left|\left\{I\right\}\right|$$
9		hashsng	$$⊢I\in V\to \left|\left\{I\right\}\right|=1$$
10	8 9	syl5eq	$$⊢I\in V\to \left|A\right|=1$$
11	10	fveq2d	$$⊢I\in V\to \left|A\right|!=1!$$
12		fac1	$$⊢1!=1$$
13	11 12	syl6eq	$$⊢I\in V\to \left|A\right|!=1$$
14	7 13	syl5eq	$$⊢I\in V\to \left|B\right|=1$$