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	No typesetting found for \|- M = ( EndoFMnd ` A ) with typecode \|-
		symgsubmefmnd.g	$⊢ G = SymGrp (A)$
		symgsubmefmnd.b	$⊢ B = {Base}_{G}$
	Assertion	symgsubmefmnd	$⊢ A \in V \to B \in SubMnd (M)$

Proof

Step	Hyp	Ref	Expression
1		symgsubmefmnd.m	Could not format M = ( EndoFMnd ` A ) : No typesetting found for \|- M = ( EndoFMnd ` A ) with typecode \|-
2		symgsubmefmnd.g	$⊢ G = SymGrp (A)$
3		symgsubmefmnd.b	$⊢ B = {Base}_{G}$
4	2 3	symgbas	$⊢ B = \{f \| f : A \underset{1-1 onto}{⟶} A\}$
5		inab	$⊢ \{f \| f : A \underset{1-1}{⟶} A\} \cap \{f \| f : A \underset{onto}{⟶} A\} = \{f \| (f : A \underset{1-1}{⟶} A \land f : A \underset{onto}{⟶} A)\}$
6		df-f1o	$⊢ f : A \underset{1-1 onto}{⟶} A \leftrightarrow (f : A \underset{1-1}{⟶} A \land f : A \underset{onto}{⟶} A)$
7	6	bicomi	$⊢ (f : A \underset{1-1}{⟶} A \land f : A \underset{onto}{⟶} A) \leftrightarrow f : A \underset{1-1 onto}{⟶} A$
8	7	abbii	$⊢ \{f \| (f : A \underset{1-1}{⟶} A \land f : A \underset{onto}{⟶} A)\} = \{f \| f : A \underset{1-1 onto}{⟶} A\}$
9	5 8	eqtr2i	$⊢ \{f \| f : A \underset{1-1 onto}{⟶} A\} = \{f \| f : A \underset{1-1}{⟶} A\} \cap \{f \| f : A \underset{onto}{⟶} A\}$
10	1	injsubmefmnd	$⊢ A \in V \to \{f \| f : A \underset{1-1}{⟶} A\} \in SubMnd (M)$
11	1	sursubmefmnd	$⊢ A \in V \to \{f \| f : A \underset{onto}{⟶} A\} \in SubMnd (M)$
12		insubm	$⊢ (\{f \| f : A \underset{1-1}{⟶} A\} \in SubMnd (M) \land \{f \| f : A \underset{onto}{⟶} A\} \in SubMnd (M)) \to \{f \| f : A \underset{1-1}{⟶} A\} \cap \{f \| f : A \underset{onto}{⟶} A\} \in SubMnd (M)$
13	10 11 12	syl2anc	$⊢ A \in V \to \{f \| f : A \underset{1-1}{⟶} A\} \cap \{f \| f : A \underset{onto}{⟶} A\} \in SubMnd (M)$
14	9 13	eqeltrid	$⊢ A \in V \to \{f \| f : A \underset{1-1 onto}{⟶} A\} \in SubMnd (M)$
15	4 14	eqeltrid	$⊢ A \in V \to B \in SubMnd (M)$