Theorem pocnv

Description: The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018)

	Ref	Expression
Assertion	pocnv	$$⊢R\mathrm{Po}A\to R^{-1}\mathrm{Po}A$$

Proof

Step	Hyp	Ref	Expression
1		poirr	$$⊢\left(R\mathrm{Po}A\wedge x\in A\right)\to \neg xRx$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2 2	brcnv	$$⊢x{R}^{-1}x\leftrightarrow xRx$$
4	1 3	sylnibr	$$⊢\left(R\mathrm{Po}A\wedge x\in A\right)\to \neg x{R}^{-1}x$$
5		3anrev	$$⊢\left(x\in A\wedge y\in A\wedge z\in A\right)\leftrightarrow \left(z\in A\wedge y\in A\wedge x\in A\right)$$
6		potr	$$⊢\left(R\mathrm{Po}A\wedge \left(z\in A\wedge y\in A\wedge x\in A\right)\right)\to \left(\left(zRy\wedge yRx\right)\to zRx\right)$$
7	5 6	sylan2b	$$⊢\left(R\mathrm{Po}A\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\right)\to \left(\left(zRy\wedge yRx\right)\to zRx\right)$$
8		vex	$$⊢y\in \mathrm{V}$$
9	2 8	brcnv	$$⊢x{R}^{-1}y\leftrightarrow yRx$$
10		vex	$$⊢z\in \mathrm{V}$$
11	8 10	brcnv	$$⊢y{R}^{-1}z\leftrightarrow zRy$$
12	9 11	anbi12ci	$$⊢\left(x{R}^{-1}y\wedge y{R}^{-1}z\right)\leftrightarrow \left(zRy\wedge yRx\right)$$
13	2 10	brcnv	$$⊢x{R}^{-1}z\leftrightarrow zRx$$
14	7 12 13	3imtr4g	$$⊢\left(R\mathrm{Po}A\wedge \left(x\in A\wedge y\in A\wedge z\in A\right)\right)\to \left(\left(x{R}^{-1}y\wedge y{R}^{-1}z\right)\to x{R}^{-1}z\right)$$
15	4 14	ispod	$$⊢R\mathrm{Po}A\to R^{-1}\mathrm{Po}A$$