This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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