Theorem psref2

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

	Ref	Expression
Assertion	psref2	$$⊢R\in \mathrm{PosetRel}\to R\cap R^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup 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	simp3d	$$⊢R\in \mathrm{PosetRel}\to R\cap R^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}$$