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 )