elcnvrefrels2

Description: Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019)

		Ref	Expression
	Assertion	elcnvrefrels2	$⊢ R \in CnvRefRels \leftrightarrow (R \subseteq I \cap (dom R \times ran R) \land R \in Rels)$

Step	Hyp	Ref	Expression
1		dfcnvrefrels2	$⊢ CnvRefRels = \{r \in Rels \| r \subseteq I \cap (dom r \times ran r)\}$
2		id	$⊢ r = R \to r = R$
3		dmeq	$⊢ r = R \to dom r = dom R$
4		rneq	$⊢ r = R \to ran r = ran R$
5	3 4	xpeq12d	$⊢ r = R \to dom r \times ran r = dom R \times ran R$
6	5	ineq2d	$⊢ r = R \to I \cap (dom r \times ran r) = I \cap (dom R \times ran R)$
7	2 6	sseq12d	$⊢ r = R \to (r \subseteq I \cap (dom r \times ran r) \leftrightarrow R \subseteq I \cap (dom R \times ran R))$
8	1 7	rabeqel	$⊢ R \in CnvRefRels \leftrightarrow (R \subseteq I \cap (dom R \times ran R) \land R \in Rels)$

Metamath Proof Explorer