Theorem tsrps

Description: A toset is a poset. (Contributed by Mario Carneiro, 9-Sep-2015)

	Ref	Expression
Assertion	tsrps	$$⊢R\in \mathrm{TosetRel}\to R\in \mathrm{PosetRel}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{dom}R=\mathrm{dom}R$$
2	1	istsr	$$⊢R\in \mathrm{TosetRel}\leftrightarrow \left(R\in \mathrm{PosetRel}\wedge \mathrm{dom}R\times \mathrm{dom}R\subseteq R\cup R^{-1}\right)$$
3	2	simplbi	$$⊢R\in \mathrm{TosetRel}\to R\in \mathrm{PosetRel}$$