Metamath Proof Explorer


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 = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) )

Proof

Step Hyp Ref Expression
1 ssidd
 |-  ( X e. _V -> { { <. X , X >. } } C_ { { <. X , X >. } } )
2 eqid
 |-  ( EndoFMnd ` { X } ) = ( EndoFMnd ` { X } )
3 eqid
 |-  ( Base ` ( EndoFMnd ` { X } ) ) = ( Base ` ( EndoFMnd ` { X } ) )
4 eqid
 |-  { X } = { X }
5 2 3 4 efmnd1bas
 |-  ( X e. _V -> ( Base ` ( EndoFMnd ` { X } ) ) = { { <. X , X >. } } )
6 eqid
 |-  ( SymGrp ` { X } ) = ( SymGrp ` { X } )
7 eqid
 |-  ( Base ` ( SymGrp ` { X } ) ) = ( Base ` ( SymGrp ` { X } ) )
8 6 7 4 symg1bas
 |-  ( X e. _V -> ( Base ` ( SymGrp ` { X } ) ) = { { <. X , X >. } } )
9 1 5 8 3sstr4d
 |-  ( X e. _V -> ( Base ` ( EndoFMnd ` { X } ) ) C_ ( Base ` ( SymGrp ` { X } ) ) )
10 fvexd
 |-  ( X e. _V -> ( EndoFMnd ` { X } ) e. _V )
11 fvexd
 |-  ( X e. _V -> ( Base ` ( SymGrp ` { X } ) ) e. _V )
12 6 7 2 symgressbas
 |-  ( SymGrp ` { X } ) = ( ( EndoFMnd ` { X } ) |`s ( Base ` ( SymGrp ` { X } ) ) )
13 12 3 ressid2
 |-  ( ( ( Base ` ( EndoFMnd ` { X } ) ) C_ ( Base ` ( SymGrp ` { X } ) ) /\ ( EndoFMnd ` { X } ) e. _V /\ ( Base ` ( SymGrp ` { X } ) ) e. _V ) -> ( SymGrp ` { X } ) = ( EndoFMnd ` { X } ) )
14 9 10 11 13 syl3anc
 |-  ( X e. _V -> ( SymGrp ` { X } ) = ( EndoFMnd ` { X } ) )
15 14 eqcomd
 |-  ( X e. _V -> ( EndoFMnd ` { X } ) = ( SymGrp ` { X } ) )
16 fveq2
 |-  ( A = { X } -> ( EndoFMnd ` A ) = ( EndoFMnd ` { X } ) )
17 fveq2
 |-  ( A = { X } -> ( SymGrp ` A ) = ( SymGrp ` { X } ) )
18 16 17 eqeq12d
 |-  ( A = { X } -> ( ( EndoFMnd ` A ) = ( SymGrp ` A ) <-> ( EndoFMnd ` { X } ) = ( SymGrp ` { X } ) ) )
19 15 18 syl5ibrcom
 |-  ( X e. _V -> ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) )
20 snprc
 |-  ( -. X e. _V <-> { X } = (/) )
21 20 biimpi
 |-  ( -. X e. _V -> { X } = (/) )
22 21 eqeq2d
 |-  ( -. X e. _V -> ( A = { X } <-> A = (/) ) )
23 0symgefmndeq
 |-  ( EndoFMnd ` (/) ) = ( SymGrp ` (/) )
24 fveq2
 |-  ( A = (/) -> ( EndoFMnd ` A ) = ( EndoFMnd ` (/) ) )
25 fveq2
 |-  ( A = (/) -> ( SymGrp ` A ) = ( SymGrp ` (/) ) )
26 23 24 25 3eqtr4a
 |-  ( A = (/) -> ( EndoFMnd ` A ) = ( SymGrp ` A ) )
27 22 26 syl6bi
 |-  ( -. X e. _V -> ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) )
28 19 27 pm2.61i
 |-  ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) )