Theorem isps

Description: The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008)

	Ref	Expression
Assertion	isps	$$⊢R\in A\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)$$

Proof

Step	Hyp	Ref	Expression
1		releq	$$⊢r=R\to \left(\mathrm{Rel}r\leftrightarrow \mathrm{Rel}R\right)$$
2		coeq1	$$⊢r=R\to r\circ r=R\circ r$$
3		coeq2	$$⊢r=R\to R\circ r=R\circ R$$
4	2 3	eqtrd	$$⊢r=R\to r\circ r=R\circ R$$
5		id	$$⊢r=R\to r=R$$
6	4 5	sseq12d	$$⊢r=R\to \left(r\circ r\subseteq r\leftrightarrow R\circ R\subseteq R\right)$$
7		cnveq	$$⊢r=R\to r^{-1}=R^{-1}$$
8	5 7	ineq12d	$$⊢r=R\to r\cap r^{-1}=R\cap R^{-1}$$
9		unieq	$$⊢r=R\to \bigcup r=\bigcup R$$
10	9	unieqd	$$⊢r=R\to \bigcup \bigcup r=\bigcup \bigcup R$$
11	10	reseq2d	$$⊢r=R\to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}$$
12	8 11	eqeq12d	$$⊢r=R\to \left(r\cap r^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\leftrightarrow R\cap R^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\right)$$
13	1 6 12	3anbi123d	$$⊢r=R\to \left(\left(\mathrm{Rel}r\wedge r\circ r\subseteq r\wedge r\cap r^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\right)\leftrightarrow \left(\mathrm{Rel}R\wedge R\circ R\subseteq R\wedge R\cap R^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\right)\right)$$
14		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\}$$
15	13 14	elab2g	$$⊢R\in A\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)$$