Metamath Proof Explorer

Theorem relcnveq2

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019)

		Ref	Expression
	Assertion	relcnveq2	$⊢ Rel R \to (R^{-1} = R \leftrightarrow \forall x \forall y (x R y \leftrightarrow y R x))$

Proof

Step	Hyp	Ref	Expression
1		cnvsym	$⊢ R^{-1} \subseteq R \leftrightarrow \forall x \forall y (x R y \to y R x)$
2	1	a1i	$⊢ Rel R \to (R^{-1} \subseteq R \leftrightarrow \forall x \forall y (x R y \to y R x))$
3		dfrel2	$⊢ Rel R \leftrightarrow {R^{-1}}^{-1} = R$
4	3	biimpi	$⊢ Rel R \to {R^{-1}}^{-1} = R$
5	4	sseq1d	$⊢ Rel R \to ({R^{-1}}^{-1} \subseteq R^{-1} \leftrightarrow R \subseteq R^{-1})$
6		cnvsym	$⊢ {R^{-1}}^{-1} \subseteq R^{-1} \leftrightarrow \forall x \forall y (x R^{-1} y \to y R^{-1} x)$
7	5 6	bitr3di	$⊢ Rel R \to (R \subseteq R^{-1} \leftrightarrow \forall x \forall y (x R^{-1} y \to y R^{-1} x))$
8		relbrcnvg	$⊢ Rel R \to (x R^{-1} y \leftrightarrow y R x)$
9		relbrcnvg	$⊢ Rel R \to (y R^{-1} x \leftrightarrow x R y)$
10	8 9	imbi12d	$⊢ Rel R \to ((x R^{-1} y \to y R^{-1} x) \leftrightarrow (y R x \to x R y))$
11	10	2albidv	$⊢ Rel R \to (\forall x \forall y (x R^{-1} y \to y R^{-1} x) \leftrightarrow \forall x \forall y (y R x \to x R y))$
12	7 11	bitrd	$⊢ Rel R \to (R \subseteq R^{-1} \leftrightarrow \forall x \forall y (y R x \to x R y))$
13	2 12	anbi12d	$⊢ Rel R \to ((R^{-1} \subseteq R \land R \subseteq R^{-1}) \leftrightarrow (\forall x \forall y (x R y \to y R x) \land \forall x \forall y (y R x \to x R y)))$
14		eqss	$⊢ R^{-1} = R \leftrightarrow (R^{-1} \subseteq R \land R \subseteq R^{-1})$
15		2albiim	$⊢ \forall x \forall y (x R y \leftrightarrow y R x) \leftrightarrow (\forall x \forall y (x R y \to y R x) \land \forall x \forall y (y R x \to x R y))$
16	13 14 15	3bitr4g	$⊢ Rel R \to (R^{-1} = R \leftrightarrow \forall x \forall y (x R y \leftrightarrow y R x))$