Metamath Proof Explorer

Theorem symggen2

Description: A finite permutation group is generated by the transpositions, see also Theorem 3.4 in Rotman p. 31. (Contributed by Stefan O'Rear, 28-Aug-2015)

		Ref	Expression
	Hypotheses	symgtrf.t	$⊢ T = ran pmTrsp (D)$
		symgtrf.g	$⊢ G = SymGrp (D)$
		symgtrf.b	$⊢ B = {Base}_{G}$
		symggen.k	$⊢ K = mrCls (SubMnd (G))$
	Assertion	symggen2	$⊢ D \in Fin \to K (T) = B$

Proof

Step	Hyp	Ref	Expression
1		symgtrf.t	$⊢ T = ran pmTrsp (D)$
2		symgtrf.g	$⊢ G = SymGrp (D)$
3		symgtrf.b	$⊢ B = {Base}_{G}$
4		symggen.k	$⊢ K = mrCls (SubMnd (G))$
5	1 2 3 4	symggen	$⊢ D \in Fin \to K (T) = \{x \in B \| dom (x ∖ I) \in Fin\}$
6		difss	$⊢ x ∖ I \subseteq x$
7		dmss	$⊢ x ∖ I \subseteq x \to dom (x ∖ I) \subseteq dom x$
8	6 7	ax-mp	$⊢ dom (x ∖ I) \subseteq dom x$
9	2 3	symgbasf1o	$⊢ x \in B \to x : D \underset{1-1 onto}{⟶} D$
10		f1odm	$⊢ x : D \underset{1-1 onto}{⟶} D \to dom x = D$
11	9 10	syl	$⊢ x \in B \to dom x = D$
12	8 11	sseqtrid	$⊢ x \in B \to dom (x ∖ I) \subseteq D$
13		ssfi	$⊢ (D \in Fin \land dom (x ∖ I) \subseteq D) \to dom (x ∖ I) \in Fin$
14	12 13	sylan2	$⊢ (D \in Fin \land x \in B) \to dom (x ∖ I) \in Fin$
15	14	ralrimiva	$⊢ D \in Fin \to \forall x \in B dom (x ∖ I) \in Fin$
16		rabid2	$⊢ B = \{x \in B \| dom (x ∖ I) \in Fin\} \leftrightarrow \forall x \in B dom (x ∖ I) \in Fin$
17	15 16	sylibr	$⊢ D \in Fin \to B = \{x \in B \| dom (x ∖ I) \in Fin\}$
18	5 17	eqtr4d	$⊢ D \in Fin \to K (T) = B$