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 ∈ V → B ∈ 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 ∩ 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 ∩ f | f : A ⟶ onto A
10 1 injsubmefmnd ⊢ A ∈ V → f | f : A ⟶ 1-1 A ∈ SubMnd ⁡ M
11 1 sursubmefmnd ⊢ A ∈ V → f | f : A ⟶ onto A ∈ SubMnd ⁡ M
12 insubm ⊢ f | f : A ⟶ 1-1 A ∈ SubMnd ⁡ M ∧ f | f : A ⟶ onto A ∈ SubMnd ⁡ M → f | f : A ⟶ 1-1 A ∩ f | f : A ⟶ onto A ∈ SubMnd ⁡ M
13 10 11 12 syl2anc ⊢ A ∈ V → f | f : A ⟶ 1-1 A ∩ f | f : A ⟶ onto A ∈ SubMnd ⁡ M
14 9 13 eqeltrid ⊢ A ∈ V → f | f : A ⟶ 1-1 onto A ∈ SubMnd ⁡ M
15 4 14 eqeltrid ⊢ A ∈ V → B ∈ SubMnd ⁡ M