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

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 e. Fin -> ( 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 e. Fin -> ( K ` T ) = { x e. B | dom ( x \ _I ) e. Fin } )
6 difss 
 |-  ( x \ _I ) C_ x
7 dmss 
 |-  ( ( x \ _I ) C_ x -> dom ( x \ _I ) C_ dom x )
8 6 7 ax-mp 
 |-  dom ( x \ _I ) C_ dom x
9 2 3 symgbasf1o 
 |-  ( x e. B -> x : D -1-1-onto-> D )
10 f1odm 
 |-  ( x : D -1-1-onto-> D -> dom x = D )
11 9 10 syl 
 |-  ( x e. B -> dom x = D )
12 8 11 sseqtrid 
 |-  ( x e. B -> dom ( x \ _I ) C_ D )
13 ssfi 
 |-  ( ( D e. Fin /\ dom ( x \ _I ) C_ D ) -> dom ( x \ _I ) e. Fin )
14 12 13 sylan2 
 |-  ( ( D e. Fin /\ x e. B ) -> dom ( x \ _I ) e. Fin )
15 14 ralrimiva 
 |-  ( D e. Fin -> A. x e. B dom ( x \ _I ) e. Fin )
16 rabid2 
 |-  ( B = { x e. B | dom ( x \ _I ) e. Fin } <-> A. x e. B dom ( x \ _I ) e. Fin )
17 15 16 sylibr 
 |-  ( D e. Fin -> B = { x e. B | dom ( x \ _I ) e. Fin } )
18 5 17 eqtr4d 
 |-  ( D e. Fin -> ( K ` T ) = B )