Theorem cnvso

Description: The converse of a strict order relation is a strict order relation. (Contributed by NM, 15-Jun-2005)

	Ref	Expression
Assertion	cnvso	$$⊢R\mathrm{Or}A\leftrightarrow R^{-1}\mathrm{Or}A$$

Proof

Step	Hyp	Ref	Expression
1		cnvpo	$$⊢R\mathrm{Po}A\leftrightarrow R^{-1}\mathrm{Po}A$$
2		ralcom	$$⊢\forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\leftrightarrow \forall y\in A\forall x\in A\left(xRy\vee x=y\vee yRx\right)$$
3		vex	$$⊢y\in \mathrm{V}$$
4		vex	$$⊢x\in \mathrm{V}$$
5	3 4	brcnv	$$⊢y{R}^{-1}x\leftrightarrow xRy$$
6		equcom	$$⊢y=x\leftrightarrow x=y$$
7	4 3	brcnv	$$⊢x{R}^{-1}y\leftrightarrow yRx$$
8	5 6 7	3orbi123i	$$⊢\left(y{R}^{-1}x\vee y=x\vee x{R}^{-1}y\right)\leftrightarrow \left(xRy\vee x=y\vee yRx\right)$$
9	8	2ralbii	$$⊢\forall y\in A\forall x\in A\left(y{R}^{-1}x\vee y=x\vee x{R}^{-1}y\right)\leftrightarrow \forall y\in A\forall x\in A\left(xRy\vee x=y\vee yRx\right)$$
10	2 9	bitr4i	$$⊢\forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\leftrightarrow \forall y\in A\forall x\in A\left(y{R}^{-1}x\vee y=x\vee x{R}^{-1}y\right)$$
11	1 10	anbi12i	$$⊢\left(R\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\right)\leftrightarrow \left(R^{-1}\mathrm{Po}A\wedge \forall y\in A\forall x\in A\left(y{R}^{-1}x\vee y=x\vee x{R}^{-1}y\right)\right)$$
12		df-so	$$⊢R\mathrm{Or}A\leftrightarrow \left(R\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\right)$$
13		df-so	$$⊢R^{-1}\mathrm{Or}A\leftrightarrow \left(R^{-1}\mathrm{Po}A\wedge \forall y\in A\forall x\in A\left(y{R}^{-1}x\vee y=x\vee x{R}^{-1}y\right)\right)$$
14	11 12 13	3bitr4i	$$⊢R\mathrm{Or}A\leftrightarrow R^{-1}\mathrm{Or}A$$