Metamath Proof Explorer

Theorem relcnveq3

Description: Two ways of saying a relation is symmetric. (Contributed by FL, 31-Aug-2009)

		Ref	Expression
	Assertion	relcnveq3	$⊢ Rel R \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 (Rel R \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 (Rel R \to \forall x \forall y (x R y \to y R x))$
6	5	com12	$⊢ Rel R \to ((R \subseteq R^{-1} \land R^{-1} \subseteq R) \to \forall x \forall y (x R y \to y R x))$
7		dfrel2	$⊢ Rel R \leftrightarrow {R^{-1}}^{-1} = R$
8		cnvss	$⊢ R^{-1} \subseteq R \to {R^{-1}}^{-1} \subseteq R^{-1}$
9		sseq1	$⊢ {R^{-1}}^{-1} = R \to ({R^{-1}}^{-1} \subseteq R^{-1} \leftrightarrow R \subseteq R^{-1})$
10	8 9	syl5ibcom	$⊢ R^{-1} \subseteq R \to ({R^{-1}}^{-1} = R \to R \subseteq R^{-1})$
11	2 10	sylbir	$⊢ \forall x \forall y (x R y \to y R x) \to ({R^{-1}}^{-1} = R \to R \subseteq R^{-1})$
12	11	com12	$⊢ {R^{-1}}^{-1} = R \to (\forall x \forall y (x R y \to y R x) \to R \subseteq R^{-1})$
13	7 12	sylbi	$⊢ Rel R \to (\forall x \forall y (x R y \to y R x) \to R \subseteq R^{-1})$
14	2	biimpri	$⊢ \forall x \forall y (x R y \to y R x) \to R^{-1} \subseteq R$
15	13 14	jca2	$⊢ Rel R \to (\forall x \forall y (x R y \to y R x) \to (R \subseteq R^{-1} \land R^{-1} \subseteq R))$
16	6 15	impbid	$⊢ Rel R \to ((R \subseteq R^{-1} \land R^{-1} \subseteq R) \leftrightarrow \forall x \forall y (x R y \to y R x))$
17	1 16	bitrid	$⊢ Rel R \to (R = R^{-1} \leftrightarrow \forall x \forall y (x R y \to y R x))$