df-symrel

Description: Define the symmetric relation predicate. (Read: R is a symmetric relation.) For sets, being an element of the class of symmetric relations ( df-symrels ) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel . Alternate definitions are dfsymrel2 and dfsymrel3 . (Contributed by Peter Mazsa, 16-Jul-2021)

		Ref	Expression
	Assertion	df-symrel	$⊢ SymRel R \leftrightarrow ({(R \cap (dom R \times ran R))}^{-1} \subseteq R \cap (dom R \times ran R) \land Rel R)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$class R$
1	0	wsymrel	$wff SymRel R$
2	0	cdm	$class dom R$
3	0	crn	$class ran R$
4	2 3	cxp	$class (dom R \times ran R)$
5	0 4	cin	$class (R \cap (dom R \times ran R))$
6	5	ccnv	$class {(R \cap (dom R \times ran R))}^{-1}$
7	6 5	wss	$wff {(R \cap (dom R \times ran R))}^{-1} \subseteq R \cap (dom R \times ran R)$
8	0	wrel	$wff Rel R$
9	7 8	wa	$wff ({(R \cap (dom R \times ran R))}^{-1} \subseteq R \cap (dom R \times ran R) \land Rel R)$
10	1 9	wb	$wff (SymRel R \leftrightarrow ({(R \cap (dom R \times ran R))}^{-1} \subseteq R \cap (dom R \times ran R) \land Rel R))$

Metamath Proof Explorer

Definition df-symrel

Detailed syntax breakdown