# 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}=\mathrm{ran}\mathrm{pmTrsp}\left({D}\right)$
symgtrf.g ${⊢}{G}=\mathrm{SymGrp}\left({D}\right)$
symgtrf.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
symggen.k ${⊢}{K}=\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)$
Assertion symggen2 ${⊢}{D}\in \mathrm{Fin}\to {K}\left({T}\right)={B}$

### Proof

Step Hyp Ref Expression
1 symgtrf.t ${⊢}{T}=\mathrm{ran}\mathrm{pmTrsp}\left({D}\right)$
2 symgtrf.g ${⊢}{G}=\mathrm{SymGrp}\left({D}\right)$
3 symgtrf.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
4 symggen.k ${⊢}{K}=\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)$
5 1 2 3 4 symggen ${⊢}{D}\in \mathrm{Fin}\to {K}\left({T}\right)=\left\{{x}\in {B}|\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$
6 difss ${⊢}{x}\setminus \mathrm{I}\subseteq {x}$
7 dmss ${⊢}{x}\setminus \mathrm{I}\subseteq {x}\to \mathrm{dom}\left({x}\setminus \mathrm{I}\right)\subseteq \mathrm{dom}{x}$
8 6 7 ax-mp ${⊢}\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\subseteq \mathrm{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 \mathrm{dom}{x}={D}$
11 9 10 syl ${⊢}{x}\in {B}\to \mathrm{dom}{x}={D}$
12 8 11 sseqtrid ${⊢}{x}\in {B}\to \mathrm{dom}\left({x}\setminus \mathrm{I}\right)\subseteq {D}$
13 ssfi ${⊢}\left({D}\in \mathrm{Fin}\wedge \mathrm{dom}\left({x}\setminus \mathrm{I}\right)\subseteq {D}\right)\to \mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}$
14 12 13 sylan2 ${⊢}\left({D}\in \mathrm{Fin}\wedge {x}\in {B}\right)\to \mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}$
15 14 ralrimiva ${⊢}{D}\in \mathrm{Fin}\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}$
16 rabid2 ${⊢}{B}=\left\{{x}\in {B}|\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}$
17 15 16 sylibr ${⊢}{D}\in \mathrm{Fin}\to {B}=\left\{{x}\in {B}|\mathrm{dom}\left({x}\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$
18 5 17 eqtr4d ${⊢}{D}\in \mathrm{Fin}\to {K}\left({T}\right)={B}$