Theorem psrel

Description: A poset is a relation. (Contributed by NM, 12-May-2008)

	Ref	Expression
Assertion	psrel	$$⊢A\in \mathrm{PosetRel}\to \mathrm{Rel}A$$

Proof

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