Theorem snsymgefmndeq

Description: The symmetric group on a singleton A is identical with the monoid of endofunctions on A . (Contributed by AV, 31-Mar-2024)

	Ref	Expression
Assertion	snsymgefmndeq	$$⊢A=\left\{X\right\}\to \mathrm{EndoFMnd}\left(A\right)=\mathrm{SymGrp}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssidd	$$⊢X\in \mathrm{V}\to \left\{\left\{⟨X,X⟩\right\}\right\}\subseteq \left\{\left\{⟨X,X⟩\right\}\right\}$$
2		eqid	$$⊢\mathrm{EndoFMnd}\left(\left\{X\right\}\right)=\mathrm{EndoFMnd}\left(\left\{X\right\}\right)$$
3		eqid	$$⊢{\mathrm{Base}}_{\mathrm{EndoFMnd}\left(\left\{X\right\}\right)}={\mathrm{Base}}_{\mathrm{EndoFMnd}\left(\left\{X\right\}\right)}$$
4		eqid	$$⊢\left\{X\right\}=\left\{X\right\}$$
5	2 3 4	efmnd1bas	$$⊢X\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{EndoFMnd}\left(\left\{X\right\}\right)}=\left\{\left\{⟨X,X⟩\right\}\right\}$$
6		eqid	$$⊢\mathrm{SymGrp}\left(\left\{X\right\}\right)=\mathrm{SymGrp}\left(\left\{X\right\}\right)$$
7		eqid	$$⊢{\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{X\right\}\right)}={\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{X\right\}\right)}$$
8	6 7 4	symg1bas	$$⊢X\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{X\right\}\right)}=\left\{\left\{⟨X,X⟩\right\}\right\}$$
9	1 5 8	3sstr4d	$$⊢X\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{EndoFMnd}\left(\left\{X\right\}\right)}\subseteq {\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{X\right\}\right)}$$
10		fvexd	$$⊢X\in \mathrm{V}\to \mathrm{EndoFMnd}\left(\left\{X\right\}\right)\in \mathrm{V}$$
11		fvexd	$$⊢X\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{X\right\}\right)}\in \mathrm{V}$$
12	6 7 2	symgressbas	$$⊢\mathrm{SymGrp}\left(\left\{X\right\}\right)=\mathrm{EndoFMnd}\left(\left\{X\right\}\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{X\right\}\right)}$$
13	12 3	ressid2	$$⊢\left({\mathrm{Base}}_{\mathrm{EndoFMnd}\left(\left\{X\right\}\right)}\subseteq {\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{X\right\}\right)}\wedge \mathrm{EndoFMnd}\left(\left\{X\right\}\right)\in \mathrm{V}\wedge {\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{X\right\}\right)}\in \mathrm{V}\right)\to \mathrm{SymGrp}\left(\left\{X\right\}\right)=\mathrm{EndoFMnd}\left(\left\{X\right\}\right)$$
14	9 10 11 13	syl3anc	$$⊢X\in \mathrm{V}\to \mathrm{SymGrp}\left(\left\{X\right\}\right)=\mathrm{EndoFMnd}\left(\left\{X\right\}\right)$$
15	14	eqcomd	$$⊢X\in \mathrm{V}\to \mathrm{EndoFMnd}\left(\left\{X\right\}\right)=\mathrm{SymGrp}\left(\left\{X\right\}\right)$$
16		fveq2	$$⊢A=\left\{X\right\}\to \mathrm{EndoFMnd}\left(A\right)=\mathrm{EndoFMnd}\left(\left\{X\right\}\right)$$
17		fveq2	$$⊢A=\left\{X\right\}\to \mathrm{SymGrp}\left(A\right)=\mathrm{SymGrp}\left(\left\{X\right\}\right)$$
18	16 17	eqeq12d	$$⊢A=\left\{X\right\}\to \left(\mathrm{EndoFMnd}\left(A\right)=\mathrm{SymGrp}\left(A\right)\leftrightarrow \mathrm{EndoFMnd}\left(\left\{X\right\}\right)=\mathrm{SymGrp}\left(\left\{X\right\}\right)\right)$$
19	15 18	syl5ibrcom	$$⊢X\in \mathrm{V}\to \left(A=\left\{X\right\}\to \mathrm{EndoFMnd}\left(A\right)=\mathrm{SymGrp}\left(A\right)\right)$$
20		snprc	$$⊢\neg X\in \mathrm{V}\leftrightarrow \left\{X\right\}=\varnothing$$
21	20	biimpi	$$⊢\neg X\in \mathrm{V}\to \left\{X\right\}=\varnothing$$
22	21	eqeq2d	$$⊢\neg X\in \mathrm{V}\to \left(A=\left\{X\right\}\leftrightarrow A=\varnothing \right)$$
23		0symgefmndeq	$$⊢\mathrm{EndoFMnd}\left(\varnothing \right)=\mathrm{SymGrp}\left(\varnothing \right)$$
24		fveq2	$$⊢A=\varnothing \to \mathrm{EndoFMnd}\left(A\right)=\mathrm{EndoFMnd}\left(\varnothing \right)$$
25		fveq2	$$⊢A=\varnothing \to \mathrm{SymGrp}\left(A\right)=\mathrm{SymGrp}\left(\varnothing \right)$$
26	23 24 25	3eqtr4a	$$⊢A=\varnothing \to \mathrm{EndoFMnd}\left(A\right)=\mathrm{SymGrp}\left(A\right)$$
27	22 26	biimtrdi	$$⊢\neg X\in \mathrm{V}\to \left(A=\left\{X\right\}\to \mathrm{EndoFMnd}\left(A\right)=\mathrm{SymGrp}\left(A\right)\right)$$
28	19 27	pm2.61i	$$⊢A=\left\{X\right\}\to \mathrm{EndoFMnd}\left(A\right)=\mathrm{SymGrp}\left(A\right)$$