Theorem symgtrf

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

	Ref	Expression
Hypotheses	symgtrf.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
	symgtrf.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
	symgtrf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	symgtrf	⊢ 𝑇 ⊆ 𝐵

Proof

Step	Hyp	Ref	Expression
1		symgtrf.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
2		symgtrf.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
3		symgtrf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
4		eqid	⊢ ( pmTrsp ‘ 𝐷 ) = ( pmTrsp ‘ 𝐷 )
5	4 1	pmtrff1o	⊢ ( 𝑥 ∈ 𝑇 → 𝑥 : 𝐷 –1-1-onto→ 𝐷 )
6	2 3	elsymgbas2	⊢ ( 𝑥 ∈ 𝑇 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 : 𝐷 –1-1-onto→ 𝐷 ) )
7	5 6	mpbird	⊢ ( 𝑥 ∈ 𝑇 → 𝑥 ∈ 𝐵 )
8	7	ssriv	⊢ 𝑇 ⊆ 𝐵