This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊆ 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 ∈ T → x : D ⟶ 1-1 onto D
6 2 3 elsymgbas2 ⊢ x ∈ T → x ∈ B ↔ x : D ⟶ 1-1 onto D
7 5 6 mpbird ⊢ x ∈ T → x ∈ B
8 7 ssriv ⊢ T ⊆ B