Metamath Proof Explorer


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
|- ( EndoFMnd ` (/) ) = ( SymGrp ` (/) )

Proof

Step Hyp Ref Expression
1 ssid
 |-  { (/) } C_ { (/) }
2 fvex
 |-  ( EndoFMnd ` (/) ) e. _V
3 p0ex
 |-  { (/) } e. _V
4 eqid
 |-  ( SymGrp ` (/) ) = ( SymGrp ` (/) )
5 symgbas0
 |-  ( Base ` ( SymGrp ` (/) ) ) = { (/) }
6 5 eqcomi
 |-  { (/) } = ( Base ` ( SymGrp ` (/) ) )
7 eqid
 |-  ( EndoFMnd ` (/) ) = ( EndoFMnd ` (/) )
8 4 6 7 symgressbas
 |-  ( SymGrp ` (/) ) = ( ( EndoFMnd ` (/) ) |`s { (/) } )
9 efmndbas0
 |-  ( Base ` ( EndoFMnd ` (/) ) ) = { (/) }
10 9 eqcomi
 |-  { (/) } = ( Base ` ( EndoFMnd ` (/) ) )
11 8 10 ressid2
 |-  ( ( { (/) } C_ { (/) } /\ ( EndoFMnd ` (/) ) e. _V /\ { (/) } e. _V ) -> ( SymGrp ` (/) ) = ( EndoFMnd ` (/) ) )
12 1 2 3 11 mp3an
 |-  ( SymGrp ` (/) ) = ( EndoFMnd ` (/) )
13 12 eqcomi
 |-  ( EndoFMnd ` (/) ) = ( SymGrp ` (/) )