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

Metamath Proof Explorer

Theorem symgsubmefmnd

Description: The symmetric group on a set A is a submonoid of the monoid of endofunctions on A . (Contributed by AV, 18-Feb-2024)

Ref Expression
Hypotheses symgsubmefmnd.m 
|- M = ( EndoFMnd ` A )
symgsubmefmnd.g 
|- G = ( SymGrp ` A )
symgsubmefmnd.b 
|- B = ( Base ` G )
Assertion symgsubmefmnd 
|- ( A e. V -> B e. ( SubMnd ` M ) )

Proof

Step Hyp Ref Expression
1 symgsubmefmnd.m 
 |-  M = ( EndoFMnd ` A )
2 symgsubmefmnd.g 
 |-  G = ( SymGrp ` A )
3 symgsubmefmnd.b 
 |-  B = ( Base ` G )
4 2 3 symgbas 
 |-  B = { f | f : A -1-1-onto-> A }
5 inab 
 |-  ( { f | f : A -1-1-> A } i^i { f | f : A -onto-> A } ) = { f | ( f : A -1-1-> A /\ f : A -onto-> A ) }
6 df-f1o 
 |-  ( f : A -1-1-onto-> A <-> ( f : A -1-1-> A /\ f : A -onto-> A ) )
7 6 bicomi 
 |-  ( ( f : A -1-1-> A /\ f : A -onto-> A ) <-> f : A -1-1-onto-> A )
8 7 abbii 
 |-  { f | ( f : A -1-1-> A /\ f : A -onto-> A ) } = { f | f : A -1-1-onto-> A }
9 5 8 eqtr2i 
 |-  { f | f : A -1-1-onto-> A } = ( { f | f : A -1-1-> A } i^i { f | f : A -onto-> A } )
10 1 injsubmefmnd 
 |-  ( A e. V -> { f | f : A -1-1-> A } e. ( SubMnd ` M ) )
11 1 sursubmefmnd 
 |-  ( A e. V -> { f | f : A -onto-> A } e. ( SubMnd ` M ) )
12 insubm 
 |-  ( ( { f | f : A -1-1-> A } e. ( SubMnd ` M ) /\ { f | f : A -onto-> A } e. ( SubMnd ` M ) ) -> ( { f | f : A -1-1-> A } i^i { f | f : A -onto-> A } ) e. ( SubMnd ` M ) )
13 10 11 12 syl2anc 
 |-  ( A e. V -> ( { f | f : A -1-1-> A } i^i { f | f : A -onto-> A } ) e. ( SubMnd ` M ) )
14 9 13 eqeltrid 
 |-  ( A e. V -> { f | f : A -1-1-onto-> A } e. ( SubMnd ` M ) )
15 4 14 eqeltrid 
 |-  ( A e. V -> B e. ( SubMnd ` M ) )