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

Metamath Proof Explorer

Theorem symgsubmefmndALT

Description: The symmetric group on a set A is a submonoid of the monoid of endofunctions on A . Alternate proof based on issubmndb and not on injsubmefmnd and sursubmefmnd . (Contributed by AV, 18-Feb-2024) (Revised by AV, 30-Mar-2024) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 symgsubmefmndALT.m 
 |-  M = ( EndoFMnd ` A )
2 symgsubmefmndALT.g 
 |-  G = ( SymGrp ` A )
3 symgsubmefmndALT.b 
 |-  B = ( Base ` G )
4 1 efmndmnd 
 |-  ( A e. V -> M e. Mnd )
5 2 3 1 symgressbas 
 |-  G = ( M |`s B )
6 2 symggrp 
 |-  ( A e. V -> G e. Grp )
7 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
8 6 7 syl 
 |-  ( A e. V -> G e. Mnd )
9 5 8 eqeltrrid 
 |-  ( A e. V -> ( M |`s B ) e. Mnd )
10 2 idresperm 
 |-  ( A e. V -> ( _I |` A ) e. ( Base ` G ) )
11 1 efmndid 
 |-  ( A e. V -> ( _I |` A ) = ( 0g ` M ) )
12 3 eqcomi 
 |-  ( Base ` G ) = B
13 12 a1i 
 |-  ( A e. V -> ( Base ` G ) = B )
14 10 11 13 3eltr3d 
 |-  ( A e. V -> ( 0g ` M ) e. B )
15 2 3 symgbasmap 
 |-  ( f e. B -> f e. ( A ^m A ) )
16 15 ssriv 
 |-  B C_ ( A ^m A )
17 eqid 
 |-  ( Base ` M ) = ( Base ` M )
18 1 17 efmndbas 
 |-  ( Base ` M ) = ( A ^m A )
19 16 18 sseqtrri 
 |-  B C_ ( Base ` M )
20 14 19 jctil 
 |-  ( A e. V -> ( B C_ ( Base ` M ) /\ ( 0g ` M ) e. B ) )
21 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
22 17 21 issubmndb 
 |-  ( B e. ( SubMnd ` M ) <-> ( ( M e. Mnd /\ ( M |`s B ) e. Mnd ) /\ ( B C_ ( Base ` M ) /\ ( 0g ` M ) e. B ) ) )
23 4 9 20 22 syl21anbrc 
 |-  ( A e. V -> B e. ( SubMnd ` M ) )