dfsymrels2

Description: Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 . (Contributed by Peter Mazsa, 20-Jul-2019)

		Ref	Expression
	Assertion	dfsymrels2	$⊢ SymRels = \{r \in Rels \| r^{-1} \subseteq r\}$

Step	Hyp	Ref	Expression
1		df-symrels	$⊢ SymRels = Syms \cap Rels$
2		df-syms	$⊢ Syms = \{r \| {(r \cap (dom r \times ran r))}^{-1} S (r \cap (dom r \times ran r))\}$
3		inex1g	$⊢ r \in V \to r \cap (dom r \times ran r) \in V$
4	3	elv	$⊢ r \cap (dom r \times ran r) \in V$
5		brssr	$⊢ r \cap (dom r \times ran r) \in V \to ({(r \cap (dom r \times ran r))}^{-1} S (r \cap (dom r \times ran r)) \leftrightarrow {(r \cap (dom r \times ran r))}^{-1} \subseteq r \cap (dom r \times ran r))$
6	4 5	ax-mp	$⊢ {(r \cap (dom r \times ran r))}^{-1} S (r \cap (dom r \times ran r)) \leftrightarrow {(r \cap (dom r \times ran r))}^{-1} \subseteq r \cap (dom r \times ran r)$
7		elrels6	$⊢ r \in V \to (r \in Rels \leftrightarrow r \cap (dom r \times ran r) = r)$
8	7	elv	$⊢ r \in Rels \leftrightarrow r \cap (dom r \times ran r) = r$
9	8	biimpi	$⊢ r \in Rels \to r \cap (dom r \times ran r) = r$
10	9	cnveqd	$⊢ r \in Rels \to {(r \cap (dom r \times ran r))}^{-1} = r^{-1}$
11	10 9	sseq12d	$⊢ r \in Rels \to ({(r \cap (dom r \times ran r))}^{-1} \subseteq r \cap (dom r \times ran r) \leftrightarrow r^{-1} \subseteq r)$
12	6 11	bitrid	$⊢ r \in Rels \to ({(r \cap (dom r \times ran r))}^{-1} S (r \cap (dom r \times ran r)) \leftrightarrow r^{-1} \subseteq r)$
13	1 2 12	abeqinbi	$⊢ SymRels = \{r \in Rels \| r^{-1} \subseteq r\}$

Metamath Proof Explorer