Metamath Proof Explorer

Theorem elrelscnveq2

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021)

		Ref	Expression
	Assertion	elrelscnveq2	$⊢ R \in Rels \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	$⊢ R \in Rels \to (R^{-1} \subseteq R \leftrightarrow \forall x \forall y (x R y \to y R x))$
3		elrelsrelim	$⊢ R \in Rels \to Rel R$
4		dfrel2	$⊢ Rel R \leftrightarrow {R^{-1}}^{-1} = R$
5	3 4	sylib	$⊢ R \in Rels \to {R^{-1}}^{-1} = R$
6	5	sseq1d	$⊢ R \in Rels \to ({R^{-1}}^{-1} \subseteq R^{-1} \leftrightarrow R \subseteq R^{-1})$
7		cnvsym	$⊢ {R^{-1}}^{-1} \subseteq R^{-1} \leftrightarrow \forall x \forall y (x R^{-1} y \to y R^{-1} x)$
8	6 7	bitr3di	$⊢ R \in Rels \to (R \subseteq R^{-1} \leftrightarrow \forall x \forall y (x R^{-1} y \to y R^{-1} x))$
9		relbrcnvg	$⊢ Rel R \to (x R^{-1} y \leftrightarrow y R x)$
10	3 9	syl	$⊢ R \in Rels \to (x R^{-1} y \leftrightarrow y R x)$
11		relbrcnvg	$⊢ Rel R \to (y R^{-1} x \leftrightarrow x R y)$
12	3 11	syl	$⊢ R \in Rels \to (y R^{-1} x \leftrightarrow x R y)$
13	10 12	imbi12d	$⊢ R \in Rels \to ((x R^{-1} y \to y R^{-1} x) \leftrightarrow (y R x \to x R y))$
14	13	2albidv	$⊢ R \in Rels \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))$
15	8 14	bitrd	$⊢ R \in Rels \to (R \subseteq R^{-1} \leftrightarrow \forall x \forall y (y R x \to x R y))$
16	2 15	anbi12d	$⊢ R \in Rels \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)))$
17		eqss	$⊢ R^{-1} = R \leftrightarrow (R^{-1} \subseteq R \land R \subseteq R^{-1})$
18		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))$
19	16 17 18	3bitr4g	$⊢ R \in Rels \to (R^{-1} = R \leftrightarrow \forall x \forall y (x R y \leftrightarrow y R x))$