Theorem cnvps

Description: The converse of a poset is a poset. In the general case (`' R e. PosetRel -> R e. PosetRel ) ` is not true. See cnvpsb for a special case where the property holds. (Contributed by FL, 5-Jan-2009) (Proof shortened by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	cnvps	$$⊢R\in \mathrm{PosetRel}\to R^{-1}\in \mathrm{PosetRel}$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{R}^{-1}$$
2	1	a1i	$$⊢R\in \mathrm{PosetRel}\to \mathrm{Rel}{R}^{-1}$$
3		cnvco	$$⊢{\left(R\circ R\right)}^{-1}=R^{-1}\circ R^{-1}$$
4		pstr2	$$⊢R\in \mathrm{PosetRel}\to R\circ R\subseteq R$$
5		cnvss	$$⊢R\circ R\subseteq R\to {\left(R\circ R\right)}^{-1}\subseteq R^{-1}$$
6	4 5	syl	$$⊢R\in \mathrm{PosetRel}\to {\left(R\circ R\right)}^{-1}\subseteq R^{-1}$$
7	3 6	eqsstrrid	$$⊢R\in \mathrm{PosetRel}\to R^{-1}\circ R^{-1}\subseteq R^{-1}$$
8		psrel	$$⊢R\in \mathrm{PosetRel}\to \mathrm{Rel}R$$
9		dfrel2	$$⊢\mathrm{Rel}R\leftrightarrow {R^{-1}}^{-1}=R$$
10	8 9	sylib	$$⊢R\in \mathrm{PosetRel}\to {R^{-1}}^{-1}=R$$
11	10	ineq2d	$$⊢R\in \mathrm{PosetRel}\to R^{-1}\cap {R^{-1}}^{-1}=R^{-1}\cap R$$
12		incom	$$⊢R^{-1}\cap R=R\cap R^{-1}$$
13	11 12	eqtrdi	$$⊢R\in \mathrm{PosetRel}\to R^{-1}\cap {R^{-1}}^{-1}=R\cap R^{-1}$$
14		psref2	$$⊢R\in \mathrm{PosetRel}\to R\cap R^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}$$
15		relcnvfld	$$⊢\mathrm{Rel}R\to \bigcup \bigcup R=\bigcup \bigcup R^{-1}$$
16	8 15	syl	$$⊢R\in \mathrm{PosetRel}\to \bigcup \bigcup R=\bigcup \bigcup R^{-1}$$
17	16	reseq2d	$$⊢R\in \mathrm{PosetRel}\to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R^{-1}}$$
18	13 14 17	3eqtrd	$$⊢R\in \mathrm{PosetRel}\to R^{-1}\cap {R^{-1}}^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R^{-1}}$$
19		cnvexg	$$⊢R\in \mathrm{PosetRel}\to R^{-1}\in \mathrm{V}$$
20		isps	$$⊢R^{-1}\in \mathrm{V}\to \left(R^{-1}\in \mathrm{PosetRel}\leftrightarrow \left(\mathrm{Rel}{R}^{-1}\wedge R^{-1}\circ R^{-1}\subseteq R^{-1}\wedge R^{-1}\cap {R^{-1}}^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R^{-1}}\right)\right)$$
21	19 20	syl	$$⊢R\in \mathrm{PosetRel}\to \left(R^{-1}\in \mathrm{PosetRel}\leftrightarrow \left(\mathrm{Rel}{R}^{-1}\wedge R^{-1}\circ R^{-1}\subseteq R^{-1}\wedge R^{-1}\cap {R^{-1}}^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R^{-1}}\right)\right)$$
22	2 7 18 21	mpbir3and	$$⊢R\in \mathrm{PosetRel}\to R^{-1}\in \mathrm{PosetRel}$$