This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfcnvrefrels2

Description: Alternate definition of the class of converse reflexive relations. See the comment of dfrefrels2 . (Contributed by Peter Mazsa, 21-Jul-2021)

		Ref	Expression
	Assertion	dfcnvrefrels2	$⊢ CnvRefRels = \{r \in Rels \| r \subseteq I \cap (dom r \times ran r)\}$

Proof

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		dmexg	$⊢ r \in V \to dom r \in V$
4	3	elv	$⊢ dom r \in V$
5		rnexg	$⊢ r \in V \to ran r \in V$
6	5	elv	$⊢ ran r \in V$
7	4 6	xpex	$⊢ dom r \times ran r \in V$
8		inex2g	$⊢ dom r \times ran r \in V \to I \cap (dom r \times ran r) \in V$
9		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))$
10	7 8 9	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)$
11		elrels6	$⊢ r \in V \to (r \in Rels \leftrightarrow r \cap (dom r \times ran r) = r)$
12	11	elv	$⊢ r \in Rels \leftrightarrow r \cap (dom r \times ran r) = r$
13	12	biimpi	$⊢ r \in Rels \to r \cap (dom r \times ran r) = r$
14	13	sseq1d	$⊢ r \in Rels \to (r \cap (dom r \times ran r) \subseteq I \cap (dom r \times ran r) \leftrightarrow r \subseteq I \cap (dom r \times ran r))$
15	10 14	bitrid	$⊢ r \in Rels \to ((I \cap (dom r \times ran r)) S^{-1} (r \cap (dom r \times ran r)) \leftrightarrow r \subseteq I \cap (dom r \times ran r))$
16	1 2 15	abeqinbi	$⊢ CnvRefRels = \{r \in Rels \| r \subseteq I \cap (dom r \times ran r)\}$