Definition df-ps

Description: Define the class of all posets (partially ordered sets) with weak ordering (e.g., "less than or equal to" instead of "less than"). A poset is a relation which is transitive, reflexive, and antisymmetric. (Contributed by NM, 11-May-2008)

	Ref	Expression
Assertion	df-ps	$$⊢\mathrm{PosetRel}=\left\{r|\left(\mathrm{Rel}r\wedge r\circ r\subseteq r\wedge r\cap r^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cps	$$class\mathrm{PosetRel}$$
1		vr	$$setvarr$$
2	1	cv	$$setvarr$$
3	2	wrel	$$wff\mathrm{Rel}r$$
4	2 2	ccom	$$class\left(r\circ r\right)$$
5	4 2	wss	$$wffr\circ r\subseteq r$$
6	2	ccnv	$$class{r}^{-1}$$
7	2 6	cin	$$class\left(r\cap r^{-1}\right)$$
8		cid	$$class\mathrm{I}$$
9	2	cuni	$$class\bigcup r$$
10	9	cuni	$$class\bigcup \bigcup r$$
11	8 10	cres	$$class\left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\right)$$
12	7 11	wceq	$$wffr\cap r^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}$$
13	3 5 12	w3a	$$wff\left(\mathrm{Rel}r\wedge r\circ r\subseteq r\wedge r\cap r^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\right)$$
14	13 1	cab	$$class\left\{r|\left(\mathrm{Rel}r\wedge r\circ r\subseteq r\wedge r\cap r^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\right)\right\}$$
15	0 14	wceq	$$wff\mathrm{PosetRel}=\left\{r|\left(\mathrm{Rel}r\wedge r\circ r\subseteq r\wedge r\cap r^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\right)\right\}$$