elrefrels2

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

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

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

Metamath Proof Explorer