Metamath Proof Explorer

Theorem dfsymrel2

Description: Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 19-Apr-2019) (Revised by Peter Mazsa, 17-Aug-2021)

		Ref	Expression
	Assertion	dfsymrel2	$⊢ SymRel R \leftrightarrow (R^{-1} \subseteq R \land Rel R)$

Proof

Step	Hyp	Ref	Expression
1		df-symrel	$⊢ SymRel R \leftrightarrow ({(R \cap (dom R \times ran R))}^{-1} \subseteq R \cap (dom R \times ran R) \land Rel R)$
2		dfrel6	$⊢ Rel R \leftrightarrow R \cap (dom R \times ran R) = R$
3	2	biimpi	$⊢ Rel R \to R \cap (dom R \times ran R) = R$
4	3	cnveqd	$⊢ Rel R \to {(R \cap (dom R \times ran R))}^{-1} = R^{-1}$
5	4 3	sseq12d	$⊢ Rel R \to ({(R \cap (dom R \times ran R))}^{-1} \subseteq R \cap (dom R \times ran R) \leftrightarrow R^{-1} \subseteq R)$
6	5	pm5.32ri	$⊢ ({(R \cap (dom R \times ran R))}^{-1} \subseteq R \cap (dom R \times ran R) \land Rel R) \leftrightarrow (R^{-1} \subseteq R \land Rel R)$
7	1 6	bitri	$⊢ SymRel R \leftrightarrow (R^{-1} \subseteq R \land Rel R)$