Theorem dfrefrel3

Description: Alternate definition of the reflexive relation predicate. A relation is reflexive iff: for all elements on its domain and range, if an element of its domain is the same as an element of its range, then there is the relation between them.

Note that this is definitely not the definition we are accustomed to, like e.g. idref / idrefALT or df-reflexive |- ( R Reflexive A <-> ( R C_ ( A X. A ) /\ A. x e. A x R x ) ) . It turns out that the not-surprising definition which contains A. x e. dom r x r x needs symmetry as well, see refsymrels3 . Only when this symmetry condition holds, like in case of equivalence relations, see dfeqvrels3 , can we write the traditional form A. x e. dom r x r x for reflexive relations. For the special case with square Cartesian product when the two forms are equivalent see idinxpssinxp4 where |- ( A. x e. A A. y e. A ( x = y -> x R y ) <-> A. x e. A x R x ) . See also similar definition of the converse reflexive relations class dfcnvrefrel3 . (Contributed by Peter Mazsa, 8-Jul-2019)

	Ref	Expression
Assertion	dfrefrel3	|- ( RefRel R <-> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ Rel R ) )

Proof

Step	Hyp	Ref	Expression
1		dfrefrel2	|- ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) )
2		idinxpss	|- ( ( _I i^i ( dom R X. ran R ) ) C_ R <-> A. x e. dom R A. y e. ran R ( x = y -> x R y ) )
3	2	anbi1i	|- ( ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) <-> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ Rel R ) )
4	1 3	bitri	|- ( RefRel R <-> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ Rel R ) )