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

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 biimtrdi 
 |-  ( -. X e. _V -> ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) ) )
28 19 27 pm2.61i 
 |-  ( A = { X } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) )