df-refrel

Description: Define the reflexive relation predicate. (Read: R is a reflexive relation.) This is a surprising definition, see the comment of dfrefrel3 . Alternate definitions are dfrefrel2 and dfrefrel3 . For sets, being an element of the class of reflexive relations ( df-refrels ) is equivalent to satisfying the reflexive relation predicate, that is ( R e. RefRels <-> RefRel R ) when R is a set, see elrefrelsrel . (Contributed by Peter Mazsa, 16-Jul-2021)

		Ref	Expression
	Assertion	df-refrel	$⊢ RefRel R \leftrightarrow (I \cap (dom R \times ran R) \subseteq R \cap (dom R \times ran R) \land Rel R)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$class R$
1	0	wrefrel	$wff RefRel R$
2		cid	$class I$
3	0	cdm	$class dom R$
4	0	crn	$class ran R$
5	3 4	cxp	$class (dom R \times ran R)$
6	2 5	cin	$class (I \cap (dom R \times ran R))$
7	0 5	cin	$class (R \cap (dom R \times ran R))$
8	6 7	wss	$wff I \cap (dom R \times ran R) \subseteq R \cap (dom R \times ran R)$
9	0	wrel	$wff Rel R$
10	8 9	wa	$wff (I \cap (dom R \times ran R) \subseteq R \cap (dom R \times ran R) \land Rel R)$
11	1 10	wb	$wff (RefRel R \leftrightarrow (I \cap (dom R \times ran R) \subseteq R \cap (dom R \times ran R) \land Rel R))$

Metamath Proof Explorer

Definition df-refrel

Detailed syntax breakdown