Theorem symg1bas

Description: The symmetric group on a singleton is the symmetric group S_1 consisting of the identity only. (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	symg1bas	$$⊢I\in V\to B=\left\{\left\{⟨I,I⟩\right\}\right\}$$

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	1 2	symgbas	$$⊢B=\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
5		eqidd	$$⊢A=\left\{I\right\}\to p=p$$
6		id	$$⊢A=\left\{I\right\}\to A=\left\{I\right\}$$
7	5 6 6	f1oeq123d	$$⊢A=\left\{I\right\}\to \left(p:A\underset{1-1\; onto}{⟶}A\leftrightarrow p:\left\{I\right\}\underset{1-1\; onto}{⟶}\left\{I\right\}\right)$$
8	3 7	ax-mp	$$⊢p:A\underset{1-1\; onto}{⟶}A\leftrightarrow p:\left\{I\right\}\underset{1-1\; onto}{⟶}\left\{I\right\}$$
9		f1of	$$⊢p:\left\{I\right\}\underset{1-1\; onto}{⟶}\left\{I\right\}\to p:\left\{I\right\}⟶\left\{I\right\}$$
10		fsng	$$⊢\left(I\in V\wedge I\in V\right)\to \left(p:\left\{I\right\}⟶\left\{I\right\}\leftrightarrow p=\left\{⟨I,I⟩\right\}\right)$$
11	10	anidms	$$⊢I\in V\to \left(p:\left\{I\right\}⟶\left\{I\right\}\leftrightarrow p=\left\{⟨I,I⟩\right\}\right)$$
12	9 11	syl5ib	$$⊢I\in V\to \left(p:\left\{I\right\}\underset{1-1\; onto}{⟶}\left\{I\right\}\to p=\left\{⟨I,I⟩\right\}\right)$$
13		f1osng	$$⊢\left(I\in V\wedge I\in V\right)\to \left\{⟨I,I⟩\right\}:\left\{I\right\}\underset{1-1\; onto}{⟶}\left\{I\right\}$$
14	13	anidms	$$⊢I\in V\to \left\{⟨I,I⟩\right\}:\left\{I\right\}\underset{1-1\; onto}{⟶}\left\{I\right\}$$
15		f1oeq1	$$⊢p=\left\{⟨I,I⟩\right\}\to \left(p:\left\{I\right\}\underset{1-1\; onto}{⟶}\left\{I\right\}\leftrightarrow \left\{⟨I,I⟩\right\}:\left\{I\right\}\underset{1-1\; onto}{⟶}\left\{I\right\}\right)$$
16	14 15	syl5ibrcom	$$⊢I\in V\to \left(p=\left\{⟨I,I⟩\right\}\to p:\left\{I\right\}\underset{1-1\; onto}{⟶}\left\{I\right\}\right)$$
17	12 16	impbid	$$⊢I\in V\to \left(p:\left\{I\right\}\underset{1-1\; onto}{⟶}\left\{I\right\}\leftrightarrow p=\left\{⟨I,I⟩\right\}\right)$$
18	8 17	syl5bb	$$⊢I\in V\to \left(p:A\underset{1-1\; onto}{⟶}A\leftrightarrow p=\left\{⟨I,I⟩\right\}\right)$$
19		vex	$$⊢p\in \mathrm{V}$$
20		f1oeq1	$$⊢f=p\to \left(f:A\underset{1-1\; onto}{⟶}A\leftrightarrow p:A\underset{1-1\; onto}{⟶}A\right)$$
21	19 20	elab	$$⊢p\in \left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\leftrightarrow p:A\underset{1-1\; onto}{⟶}A$$
22		velsn	$$⊢p\in \left\{\left\{⟨I,I⟩\right\}\right\}\leftrightarrow p=\left\{⟨I,I⟩\right\}$$
23	18 21 22	3bitr4g	$$⊢I\in V\to \left(p\in \left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\leftrightarrow p\in \left\{\left\{⟨I,I⟩\right\}\right\}\right)$$
24	23	eqrdv	$$⊢I\in V\to \left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}=\left\{\left\{⟨I,I⟩\right\}\right\}$$
25	4 24	syl5eq	$$⊢I\in V\to B=\left\{\left\{⟨I,I⟩\right\}\right\}$$