df-cnvrefrel

Description: Define the converse reflexive relation predicate (read: R is a converse reflexive relation), see also the comment of dfcnvrefrel3 . Alternate definitions are dfcnvrefrel2 and dfcnvrefrel3 . (Contributed by Peter Mazsa, 16-Jul-2021)

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

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-cnvrefrel

Detailed syntax breakdown