Metamath Proof Explorer


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