Theorem pstr2

Description: A poset is transitive. (Contributed by FL, 3-Aug-2009)

	Ref	Expression
Assertion	pstr2	$$⊢R\in \mathrm{PosetRel}\to R\circ R\subseteq R$$

Proof

Step	Hyp	Ref	Expression
1		isps	$$⊢R\in \mathrm{PosetRel}\to \left(R\in \mathrm{PosetRel}\leftrightarrow \left(\mathrm{Rel}R\wedge R\circ R\subseteq R\wedge R\cap R^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\right)\right)$$
2	1	ibi	$$⊢R\in \mathrm{PosetRel}\to \left(\mathrm{Rel}R\wedge R\circ R\subseteq R\wedge R\cap R^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\right)$$
3	2	simp2d	$$⊢R\in \mathrm{PosetRel}\to R\circ R\subseteq R$$