Theorem psgnfitr

Description: A permutation of a finite set is generated by transpositions. (Contributed by AV, 13-Jan-2019)

	Ref	Expression
Hypotheses	psgnfitr.g	|- G = ( SymGrp ` N )
	psgnfitr.p	|- B = ( Base ` G )
	psgnfitr.t	|- T = ran ( pmTrsp ` N )
Assertion	psgnfitr	|- ( N e. Fin -> ( Q e. B <-> E. w e. Word T Q = ( G gsum w ) ) )

Proof

Step	Hyp	Ref	Expression
1		psgnfitr.g	|- G = ( SymGrp ` N )
2		psgnfitr.p	|- B = ( Base ` G )
3		psgnfitr.t	|- T = ran ( pmTrsp ` N )
4		eqid	|- ( mrCls ` ( SubMnd ` G ) ) = ( mrCls ` ( SubMnd ` G ) )
5	3 1 2 4	symggen2	|- ( N e. Fin -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = B )
6	1	symggrp	|- ( N e. Fin -> G e. Grp )
7		grpmnd	|- ( G e. Grp -> G e. Mnd )
8	6 7	syl	|- ( N e. Fin -> G e. Mnd )
9		eqid	|- ( Base ` G ) = ( Base ` G )
10	3 1 9	symgtrf	|- T C_ ( Base ` G )
11	9 4	gsumwspan	|- ( ( G e. Mnd /\ T C_ ( Base ` G ) ) -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = ran ( w e. Word T |-> ( G gsum w ) ) )
12	8 10 11	sylancl	|- ( N e. Fin -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = ran ( w e. Word T |-> ( G gsum w ) ) )
13	5 12	eqtr3d	|- ( N e. Fin -> B = ran ( w e. Word T |-> ( G gsum w ) ) )
14	13	eleq2d	|- ( N e. Fin -> ( Q e. B <-> Q e. ran ( w e. Word T |-> ( G gsum w ) ) ) )
15		eqid	|- ( w e. Word T |-> ( G gsum w ) ) = ( w e. Word T |-> ( G gsum w ) )
16		ovex	|- ( G gsum w ) e. _V
17	15 16	elrnmpti	|- ( Q e. ran ( w e. Word T |-> ( G gsum w ) ) <-> E. w e. Word T Q = ( G gsum w ) )
18	14 17	bitrdi	|- ( N e. Fin -> ( Q e. B <-> E. w e. Word T Q = ( G gsum w ) ) )