Theorem cnvsymOLD

Description: Obsolete proof of cnvsym as of 29-Dec-2024. (Contributed by NM, 28-Dec-1996) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by SN, 23-Dec-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	cnvsymOLD	$$⊢R^{-1}\subseteq R\leftrightarrow \forall x\forall y\left(xRy\to yRx\right)$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{R}^{-1}$$
2		ssrel3	$$⊢\mathrm{Rel}{R}^{-1}\to \left(R^{-1}\subseteq R\leftrightarrow \forall y\forall x\left(y{R}^{-1}x\to yRx\right)\right)$$
3	1 2	ax-mp	$$⊢R^{-1}\subseteq R\leftrightarrow \forall y\forall x\left(y{R}^{-1}x\to yRx\right)$$
4		alcom	$$⊢\forall y\forall x\left(y{R}^{-1}x\to yRx\right)\leftrightarrow \forall x\forall y\left(y{R}^{-1}x\to yRx\right)$$
5		vex	$$⊢y\in \mathrm{V}$$
6		vex	$$⊢x\in \mathrm{V}$$
7	5 6	brcnv	$$⊢y{R}^{-1}x\leftrightarrow xRy$$
8	7	imbi1i	$$⊢\left(y{R}^{-1}x\to yRx\right)\leftrightarrow \left(xRy\to yRx\right)$$
9	8	2albii	$$⊢\forall x\forall y\left(y{R}^{-1}x\to yRx\right)\leftrightarrow \forall x\forall y\left(xRy\to yRx\right)$$
10	3 4 9	3bitri	$$⊢R^{-1}\subseteq R\leftrightarrow \forall x\forall y\left(xRy\to yRx\right)$$