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	6	grpmndd	|- ( N e. Fin -> G e. Mnd )
8		eqid	|- ( Base ` G ) = ( Base ` G )
9	3 1 8	symgtrf	|- T C_ ( Base ` G )
10	8 4	gsumwspan	|- ( ( G e. Mnd /\ T C_ ( Base ` G ) ) -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = ran ( w e. Word T |-> ( G gsum w ) ) )
11	7 9 10	sylancl	|- ( N e. Fin -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = ran ( w e. Word T |-> ( G gsum w ) ) )
12	5 11	eqtr3d	|- ( N e. Fin -> B = ran ( w e. Word T |-> ( G gsum w ) ) )
13	12	eleq2d	|- ( N e. Fin -> ( Q e. B <-> Q e. ran ( w e. Word T |-> ( G gsum w ) ) ) )
14		eqid	|- ( w e. Word T |-> ( G gsum w ) ) = ( w e. Word T |-> ( G gsum w ) )
15		ovex	|- ( G gsum w ) e. _V
16	14 15	elrnmpti	|- ( Q e. ran ( w e. Word T |-> ( G gsum w ) ) <-> E. w e. Word T Q = ( G gsum w ) )
17	13 16	bitrdi	|- ( N e. Fin -> ( Q e. B <-> E. w e. Word T Q = ( G gsum w ) ) )