dfcnvrefrels3

Description: Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019)

		Ref	Expression
	Assertion	dfcnvrefrels3	$⊢ CnvRefRels = \{r \in Rels \| \forall x \in dom r \forall y \in ran r (x r y \to x = y)\}$

Step	Hyp	Ref	Expression
1		df-cnvrefrels	$⊢ CnvRefRels = CnvRefs \cap Rels$
2		df-cnvrefs	$⊢ CnvRefs = \{r \| (I \cap (dom r \times ran r)) S^{-1} (r \cap (dom r \times ran r))\}$
3	1 2	abeqin	$⊢ CnvRefRels = \{r \in Rels \| (I \cap (dom r \times ran r)) S^{-1} (r \cap (dom r \times ran r))\}$
4		dmexg	$⊢ r \in V \to dom r \in V$
5	4	elv	$⊢ dom r \in V$
6		rnexg	$⊢ r \in V \to ran r \in V$
7	6	elv	$⊢ ran r \in V$
8	5 7	xpex	$⊢ dom r \times ran r \in V$
9		inex2g	$⊢ dom r \times ran r \in V \to I \cap (dom r \times ran r) \in V$
10		brcnvssr	$⊢ I \cap (dom r \times ran r) \in V \to ((I \cap (dom r \times ran r)) S^{-1} (r \cap (dom r \times ran r)) \leftrightarrow r \cap (dom r \times ran r) \subseteq I \cap (dom r \times ran r))$
11	8 9 10	mp2b	$⊢ (I \cap (dom r \times ran r)) S^{-1} (r \cap (dom r \times ran r)) \leftrightarrow r \cap (dom r \times ran r) \subseteq I \cap (dom r \times ran r)$
12		inxpssidinxp	$⊢ r \cap (dom r \times ran r) \subseteq I \cap (dom r \times ran r) \leftrightarrow \forall x \in dom r \forall y \in ran r (x r y \to x = y)$
13	11 12	bitri	$⊢ (I \cap (dom r \times ran r)) S^{-1} (r \cap (dom r \times ran r)) \leftrightarrow \forall x \in dom r \forall y \in ran r (x r y \to x = y)$
14	3 13	rabbieq	$⊢ CnvRefRels = \{r \in Rels \| \forall x \in dom r \forall y \in ran r (x r y \to x = y)\}$

Metamath Proof Explorer