dfcnvrefrel3

Description: Alternate definition of the converse reflexive relation predicate. A relation is converse reflexive iff: for all elements on its domain and range, if for an element of its domain and for an element of its range there is the relation between them, then the two elements are the same, cf. the comment of dfrefrel3 . (Contributed by Peter Mazsa, 25-Jul-2021)

		Ref	Expression
	Assertion	dfcnvrefrel3	$⊢ CnvRefRel R \leftrightarrow (\forall x \in dom R \forall y \in ran R (x R y \to x = y) \land Rel R)$

Proof

Step	Hyp	Ref	Expression
1		df-cnvrefrel	$⊢ CnvRefRel R \leftrightarrow (R \cap (dom R \times ran R) \subseteq I \cap (dom R \times ran R) \land Rel R)$
2		inxpssidinxp	$⊢ R \cap (dom R \times ran R) \subseteq I \cap (dom R \times ran R) \leftrightarrow \forall x \in dom R \forall y \in ran R (x R y \to x = y)$
3	2	anbi1i	$⊢ (R \cap (dom R \times ran R) \subseteq I \cap (dom R \times ran R) \land Rel R) \leftrightarrow (\forall x \in dom R \forall y \in ran R (x R y \to x = y) \land Rel R)$
4	1 3	bitri	$⊢ CnvRefRel R \leftrightarrow (\forall x \in dom R \forall y \in ran R (x R y \to x = y) \land Rel R)$

Metamath Proof Explorer

Theorem dfcnvrefrel3

Proof