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

Metamath Proof Explorer

Theorem tsrps

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

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

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