Theorem 0symgefmndeq

Description: The symmetric group on the empty set is identical with the monoid of endofunctions on the empty set. (Contributed by AV, 30-Mar-2024)

	Ref	Expression
Assertion	0symgefmndeq	Could not format assertion : No typesetting found for |- ( EndoFMnd ` (/) ) = ( SymGrp ` (/) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢\left\{\varnothing \right\}\subseteq \left\{\varnothing \right\}$$
2		fvex	Could not format ( EndoFMnd ` (/) ) e. _V : No typesetting found for |- ( EndoFMnd ` (/) ) e. _V with typecode |-
3		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
4		eqid	$$⊢\mathrm{SymGrp}\left(\varnothing \right)=\mathrm{SymGrp}\left(\varnothing \right)$$
5		symgbas0	$$⊢{\mathrm{Base}}_{\mathrm{SymGrp}\left(\varnothing \right)}=\left\{\varnothing \right\}$$
6	5	eqcomi	$$⊢\left\{\varnothing \right\}={\mathrm{Base}}_{\mathrm{SymGrp}\left(\varnothing \right)}$$
7		eqid	Could not format ( EndoFMnd ` (/) ) = ( EndoFMnd ` (/) ) : No typesetting found for |- ( EndoFMnd ` (/) ) = ( EndoFMnd ` (/) ) with typecode |-
8	4 6 7	symgressbas	Could not format ( SymGrp ` (/) ) = ( ( EndoFMnd ` (/) ) |`s { (/) } ) : No typesetting found for |- ( SymGrp ` (/) ) = ( ( EndoFMnd ` (/) ) |`s { (/) } ) with typecode |-
9		efmndbas0	Could not format ( Base ` ( EndoFMnd ` (/) ) ) = { (/) } : No typesetting found for |- ( Base ` ( EndoFMnd ` (/) ) ) = { (/) } with typecode |-
10	9	eqcomi	Could not format { (/) } = ( Base ` ( EndoFMnd ` (/) ) ) : No typesetting found for |- { (/) } = ( Base ` ( EndoFMnd ` (/) ) ) with typecode |-
11	8 10	ressid2	Could not format ( ( { (/) } C_ { (/) } /\ ( EndoFMnd ` (/) ) e. _V /\ { (/) } e. _V ) -> ( SymGrp ` (/) ) = ( EndoFMnd ` (/) ) ) : No typesetting found for |- ( ( { (/) } C_ { (/) } /\ ( EndoFMnd ` (/) ) e. _V /\ { (/) } e. _V ) -> ( SymGrp ` (/) ) = ( EndoFMnd ` (/) ) ) with typecode |-
12	1 2 3 11	mp3an	Could not format ( SymGrp ` (/) ) = ( EndoFMnd ` (/) ) : No typesetting found for |- ( SymGrp ` (/) ) = ( EndoFMnd ` (/) ) with typecode |-
13	12	eqcomi	Could not format ( EndoFMnd ` (/) ) = ( SymGrp ` (/) ) : No typesetting found for |- ( EndoFMnd ` (/) ) = ( SymGrp ` (/) ) with typecode |-