Theorem cnvsym

Description: Two ways of saying a relation is symmetric. Similar to definition of symmetry in Schechter p. 51. (Contributed by NM, 28-Dec-1996) (Proof shortened by Andrew Salmon, 27-Aug-2011)

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

Proof

Step	Hyp	Ref	Expression
1		alcom	$$⊢\forall y\forall x\left(⟨y,x⟩\in R^{-1}\to ⟨y,x⟩\in R\right)\leftrightarrow \forall x\forall y\left(⟨y,x⟩\in R^{-1}\to ⟨y,x⟩\in R\right)$$
2		relcnv	$$⊢\mathrm{Rel}{R}^{-1}$$
3		ssrel	$$⊢\mathrm{Rel}{R}^{-1}\to \left(R^{-1}\subseteq R\leftrightarrow \forall y\forall x\left(⟨y,x⟩\in R^{-1}\to ⟨y,x⟩\in R\right)\right)$$
4	2 3	ax-mp	$$⊢R^{-1}\subseteq R\leftrightarrow \forall y\forall x\left(⟨y,x⟩\in R^{-1}\to ⟨y,x⟩\in R\right)$$
5		vex	$$⊢y\in \mathrm{V}$$
6		vex	$$⊢x\in \mathrm{V}$$
7	5 6	brcnv	$$⊢y{R}^{-1}x\leftrightarrow xRy$$
8		df-br	$$⊢y{R}^{-1}x\leftrightarrow ⟨y,x⟩\in R^{-1}$$
9	7 8	bitr3i	$$⊢xRy\leftrightarrow ⟨y,x⟩\in R^{-1}$$
10		df-br	$$⊢yRx\leftrightarrow ⟨y,x⟩\in R$$
11	9 10	imbi12i	$$⊢\left(xRy\to yRx\right)\leftrightarrow \left(⟨y,x⟩\in R^{-1}\to ⟨y,x⟩\in R\right)$$
12	11	2albii	$$⊢\forall x\forall y\left(xRy\to yRx\right)\leftrightarrow \forall x\forall y\left(⟨y,x⟩\in R^{-1}\to ⟨y,x⟩\in R\right)$$
13	1 4 12	3bitr4i	$$⊢R^{-1}\subseteq R\leftrightarrow \forall x\forall y\left(xRy\to yRx\right)$$