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

Metamath Proof Explorer

Theorem symgcl

Description: The group operation of the symmetric group on A is closed, i.e. a magma. (Contributed by Mario Carneiro, 12-Jan-2015) (Revised by Mario Carneiro, 28-Jan-2015)

		Ref	Expression
	Hypotheses	symgov.1	$⊢ G = SymGrp (A)$
		symgov.2	$⊢ B = {Base}_{G}$
		symgov.3	$⊢ \underset{˙}{+} = +_{G}$
	Assertion	symgcl	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$

Proof

Step	Hyp	Ref	Expression
1		symgov.1	$⊢ G = SymGrp (A)$
2		symgov.2	$⊢ B = {Base}_{G}$
3		symgov.3	$⊢ \underset{˙}{+} = +_{G}$
4	1 2 3	symgov	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{+} Y = X \circ Y$
5	1 2	symgbasf1o	$⊢ X \in B \to X : A \underset{1-1 onto}{⟶} A$
6	1 2	symgbasf1o	$⊢ Y \in B \to Y : A \underset{1-1 onto}{⟶} A$
7		f1oco	$⊢ (X : A \underset{1-1 onto}{⟶} A \land Y : A \underset{1-1 onto}{⟶} A) \to (X \circ Y) : A \underset{1-1 onto}{⟶} A$
8	5 6 7	syl2an	$⊢ (X \in B \land Y \in B) \to (X \circ Y) : A \underset{1-1 onto}{⟶} A$
9		coexg	$⊢ (X \in B \land Y \in B) \to X \circ Y \in V$
10	1 2	elsymgbas2	$⊢ X \circ Y \in V \to (X \circ Y \in B \leftrightarrow (X \circ Y) : A \underset{1-1 onto}{⟶} A)$
11	9 10	syl	$⊢ (X \in B \land Y \in B) \to (X \circ Y \in B \leftrightarrow (X \circ Y) : A \underset{1-1 onto}{⟶} A)$
12	8 11	mpbird	$⊢ (X \in B \land Y \in B) \to X \circ Y \in B$
13	4 12	eqeltrd	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$