Theorem symgtrf

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

	Ref	Expression
Hypotheses	symgtrf.t	$$⊢T=\mathrm{ran}\mathrm{pmTrsp}\left(D\right)$$
	symgtrf.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
	symgtrf.b	$$⊢B={\mathrm{Base}}_G$$
Assertion	symgtrf	$$⊢T\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		symgtrf.t	$$⊢T=\mathrm{ran}\mathrm{pmTrsp}\left(D\right)$$
2		symgtrf.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
3		symgtrf.b	$$⊢B={\mathrm{Base}}_G$$
4		eqid	$$⊢\mathrm{pmTrsp}\left(D\right)=\mathrm{pmTrsp}\left(D\right)$$
5	4 1	pmtrff1o	$$⊢x\in T\to x:D\underset{1-1\; onto}{⟶}D$$
6	2 3	elsymgbas2	$$⊢x\in T\to \left(x\in B\leftrightarrow x:D\underset{1-1\; onto}{⟶}D\right)$$
7	5 6	mpbird	$$⊢x\in T\to x\in B$$
8	7	ssriv	$$⊢T\subseteq B$$