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 No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
symgsubmefmndALT.g ⊢G=SymGrp⁡A
symgsubmefmndALT.b ⊢B=BaseG
Assertion symgsubmefmndALT ⊢A∈V→B∈SubMnd⁡M

Proof

Step Hyp Ref Expression
1 symgsubmefmndALT.m Could not format M = ( EndoFMnd ` A ) : No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
2 symgsubmefmndALT.g ⊢G=SymGrp⁡A
3 symgsubmefmndALT.b ⊢B=BaseG
4 1 efmndmnd ⊢A∈V→M∈Mnd
5 2 3 1 symgressbas ⊢G=M↾𝑠B
6 2 symggrp ⊢A∈V→G∈Grp
7 grpmnd ⊢G∈Grp→G∈Mnd
8 6 7 syl ⊢A∈V→G∈Mnd
9 5 8 eqeltrrid ⊢A∈V→M↾𝑠B∈Mnd
10 2 idresperm ⊢A∈V→I↾A∈BaseG
11 1 efmndid ⊢A∈V→I↾A=0M
12 3 eqcomi ⊢BaseG=B
13 12 a1i ⊢A∈V→BaseG=B
14 10 11 13 3eltr3d ⊢A∈V→0M∈B
15 2 3 symgbasmap ⊢f∈B→f∈AA
16 15 ssriv ⊢B⊆AA
17 eqid ⊢BaseM=BaseM
18 1 17 efmndbas ⊢BaseM=AA
19 16 18 sseqtrri ⊢B⊆BaseM
20 14 19 jctil ⊢A∈V→B⊆BaseM∧0M∈B
21 eqid ⊢0M=0M
22 17 21 issubmndb ⊢B∈SubMnd⁡M↔M∈Mnd∧M↾𝑠B∈Mnd∧B⊆BaseM∧0M∈B
23 4 9 20 22 syl21anbrc ⊢A∈V→B∈SubMnd⁡M