Metamath Proof Explorer

Theorem elrelscnveq3

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

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

Proof

Step	Hyp	Ref	Expression
1		eqss	$⊢ R = R^{-1} \leftrightarrow (R \subseteq R^{-1} \land R^{-1} \subseteq R)$
2		cnvsym	$⊢ R^{-1} \subseteq R \leftrightarrow \forall x \forall y (x R y \to y R x)$
3	2	biimpi	$⊢ R^{-1} \subseteq R \to \forall x \forall y (x R y \to y R x)$
4	3	a1d	$⊢ R^{-1} \subseteq R \to (R \in Rels \to \forall x \forall y (x R y \to y R x))$
5	4	adantl	$⊢ (R \subseteq R^{-1} \land R^{-1} \subseteq R) \to (R \in Rels \to \forall x \forall y (x R y \to y R x))$
6	5	com12	$⊢ R \in Rels \to ((R \subseteq R^{-1} \land R^{-1} \subseteq R) \to \forall x \forall y (x R y \to y R x))$
7		elrelsrelim	$⊢ R \in Rels \to Rel R$
8		dfrel2	$⊢ Rel R \leftrightarrow {R^{-1}}^{-1} = R$
9	7 8	sylib	$⊢ R \in Rels \to {R^{-1}}^{-1} = R$
10		cnvss	$⊢ R^{-1} \subseteq R \to {R^{-1}}^{-1} \subseteq R^{-1}$
11		sseq1	$⊢ {R^{-1}}^{-1} = R \to ({R^{-1}}^{-1} \subseteq R^{-1} \leftrightarrow R \subseteq R^{-1})$
12	10 11	syl5ibcom	$⊢ R^{-1} \subseteq R \to ({R^{-1}}^{-1} = R \to R \subseteq R^{-1})$
13	2 12	sylbir	$⊢ \forall x \forall y (x R y \to y R x) \to ({R^{-1}}^{-1} = R \to R \subseteq R^{-1})$
14	9 13	syl5com	$⊢ R \in Rels \to (\forall x \forall y (x R y \to y R x) \to R \subseteq R^{-1})$
15	2	biimpri	$⊢ \forall x \forall y (x R y \to y R x) \to R^{-1} \subseteq R$
16	14 15	jca2	$⊢ R \in Rels \to (\forall x \forall y (x R y \to y R x) \to (R \subseteq R^{-1} \land R^{-1} \subseteq R))$
17	6 16	impbid	$⊢ R \in Rels \to ((R \subseteq R^{-1} \land R^{-1} \subseteq R) \leftrightarrow \forall x \forall y (x R y \to y R x))$
18	1 17	bitrid	$⊢ R \in Rels \to (R = R^{-1} \leftrightarrow \forall x \forall y (x R y \to y R x))$