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	Could not format assertion : No typesetting found for |- ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) with typecode |-

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	Could not format ( EndoFMnd ` { X } ) = ( EndoFMnd ` { X } ) : No typesetting found for |- ( EndoFMnd ` { X } ) = ( EndoFMnd ` { X } ) with typecode |-
3		eqid	Could not format ( Base ` ( EndoFMnd ` { X } ) ) = ( Base ` ( EndoFMnd ` { X } ) ) : No typesetting found for |- ( Base ` ( EndoFMnd ` { X } ) ) = ( Base ` ( EndoFMnd ` { X } ) ) with typecode |-
4		eqid	$$⊢\left\{X\right\}=\left\{X\right\}$$
5	2 3 4	efmnd1bas	Could not format ( X e. _V -> ( Base ` ( EndoFMnd ` { X } ) ) = { { <. X , X >. } } ) : No typesetting found for |- ( X e. _V -> ( Base ` ( EndoFMnd ` { X } ) ) = { { <. X , X >. } } ) with typecode |-
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	Could not format ( X e. _V -> ( Base ` ( EndoFMnd ` { X } ) ) C_ ( Base ` ( SymGrp ` { X } ) ) ) : No typesetting found for |- ( X e. _V -> ( Base ` ( EndoFMnd ` { X } ) ) C_ ( Base ` ( SymGrp ` { X } ) ) ) with typecode |-
10		fvexd	Could not format ( X e. _V -> ( EndoFMnd ` { X } ) e. _V ) : No typesetting found for |- ( X e. _V -> ( EndoFMnd ` { X } ) e. _V ) with typecode |-
11		fvexd	$$⊢X\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{SymGrp}\left(\left\{X\right\}\right)}\in \mathrm{V}$$
12	6 7 2	symgressbas	Could not format ( SymGrp ` { X } ) = ( ( EndoFMnd ` { X } ) |`s ( Base ` ( SymGrp ` { X } ) ) ) : No typesetting found for |- ( SymGrp ` { X } ) = ( ( EndoFMnd ` { X } ) |`s ( Base ` ( SymGrp ` { X } ) ) ) with typecode |-
13	12 3	ressid2	Could not format ( ( ( Base ` ( EndoFMnd ` { X } ) ) C_ ( Base ` ( SymGrp ` { X } ) ) /\ ( EndoFMnd ` { X } ) e. _V /\ ( Base ` ( SymGrp ` { X } ) ) e. _V ) -> ( SymGrp ` { X } ) = ( EndoFMnd ` { X } ) ) : No typesetting found for |- ( ( ( Base ` ( EndoFMnd ` { X } ) ) C_ ( Base ` ( SymGrp ` { X } ) ) /\ ( EndoFMnd ` { X } ) e. _V /\ ( Base ` ( SymGrp ` { X } ) ) e. _V ) -> ( SymGrp ` { X } ) = ( EndoFMnd ` { X } ) ) with typecode |-
14	9 10 11 13	syl3anc	Could not format ( X e. _V -> ( SymGrp ` { X } ) = ( EndoFMnd ` { X } ) ) : No typesetting found for |- ( X e. _V -> ( SymGrp ` { X } ) = ( EndoFMnd ` { X } ) ) with typecode |-
15	14	eqcomd	Could not format ( X e. _V -> ( EndoFMnd ` { X } ) = ( SymGrp ` { X } ) ) : No typesetting found for |- ( X e. _V -> ( EndoFMnd ` { X } ) = ( SymGrp ` { X } ) ) with typecode |-
16		fveq2	Could not format ( A = { X } -> ( EndoFMnd ` A ) = ( EndoFMnd ` { X } ) ) : No typesetting found for |- ( A = { X } -> ( EndoFMnd ` A ) = ( EndoFMnd ` { X } ) ) with typecode |-
17		fveq2	$$⊢A=\left\{X\right\}\to \mathrm{SymGrp}\left(A\right)=\mathrm{SymGrp}\left(\left\{X\right\}\right)$$
18	16 17	eqeq12d	Could not format ( A = { X } -> ( ( EndoFMnd ` A ) = ( SymGrp ` A ) <-> ( EndoFMnd ` { X } ) = ( SymGrp ` { X } ) ) ) : No typesetting found for |- ( A = { X } -> ( ( EndoFMnd ` A ) = ( SymGrp ` A ) <-> ( EndoFMnd ` { X } ) = ( SymGrp ` { X } ) ) ) with typecode |-
19	15 18	syl5ibrcom	Could not format ( X e. _V -> ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) ) : No typesetting found for |- ( X e. _V -> ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) ) with typecode |-
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	Could not format ( EndoFMnd ` (/) ) = ( SymGrp ` (/) ) : No typesetting found for |- ( EndoFMnd ` (/) ) = ( SymGrp ` (/) ) with typecode |-
24		fveq2	Could not format ( A = (/) -> ( EndoFMnd ` A ) = ( EndoFMnd ` (/) ) ) : No typesetting found for |- ( A = (/) -> ( EndoFMnd ` A ) = ( EndoFMnd ` (/) ) ) with typecode |-
25		fveq2	$$⊢A=\varnothing \to \mathrm{SymGrp}\left(A\right)=\mathrm{SymGrp}\left(\varnothing \right)$$
26	23 24 25	3eqtr4a	Could not format ( A = (/) -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) : No typesetting found for |- ( A = (/) -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) with typecode |-
27	22 26	syl6bi	Could not format ( -. X e. _V -> ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) ) : No typesetting found for |- ( -. X e. _V -> ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) ) with typecode |-
28	19 27	pm2.61i	Could not format ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) : No typesetting found for |- ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) with typecode |-