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 |
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 |