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 = Base G
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 = Base G
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 ∈ Base G
11 1 efmndid ⊢ A ∈ V → I ↾ A = 0 M
12 3 eqcomi ⊢ Base G = B
13 12 a1i ⊢ A ∈ V → Base G = B
14 10 11 13 3eltr3d ⊢ A ∈ V → 0 M ∈ B
15 2 3 symgbasmap ⊢ f ∈ B → f ∈ A A
16 15 ssriv ⊢ B ⊆ A A
17 eqid ⊢ Base M = Base M
18 1 17 efmndbas ⊢ Base M = A A
19 16 18 sseqtrri ⊢ B ⊆ Base M
20 14 19 jctil ⊢ A ∈ V → B ⊆ Base M ∧ 0 M ∈ B
21 eqid ⊢ 0 M = 0 M
22 17 21 issubmndb ⊢ B ∈ SubMnd ⁡ M ↔ M ∈ Mnd ∧ M ↾ 𝑠 B ∈ Mnd ∧ B ⊆ Base M ∧ 0 M ∈ B
23 4 9 20 22 syl21anbrc ⊢ A ∈ V → B ∈ SubMnd ⁡ M