Theorem symgtrf

Description: Transpositions are elements of the symmetric group. (Contributed by Stefan O'Rear, 23-Aug-2015)

	Ref	Expression
Hypotheses	symgtrf.t	|- T = ran ( pmTrsp ` D )
	symgtrf.g	|- G = ( SymGrp ` D )
	symgtrf.b	|- B = ( Base ` G )
Assertion	symgtrf	|- T C_ 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		eqid	|- ( pmTrsp ` D ) = ( pmTrsp ` D )
5	4 1	pmtrff1o	|- ( x e. T -> x : D -1-1-onto-> D )
6	2 3	elsymgbas2	|- ( x e. T -> ( x e. B <-> x : D -1-1-onto-> D ) )
7	5 6	mpbird	|- ( x e. T -> x e. B )
8	7	ssriv	|- T C_ B