refrel cnvrefrel symrel refsymrel (#2531)
refrel cnvrefrel symrel refsymrel (#2531)

4 sections: Reflexivity, Converse reflexivity, Symmetry, Reflexivity and symmetry.

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 ( ~ dfrefrel3 ).

This definition is surprising: the conventional definition with the x R x part may be the result of that reflexivity is perceived primarily as a necessary part of equivalence. This seems to be the main reason why we thought so far that reflexivity on its own should be defined like the reflexivity part of ~~? dfeqvrel3 , i.e., by using the apparently self-evident x R x form, cf. section "Reflexivity and symmetry" below.

Another possible reason is that we are inclined to constrain ourselves to convenient special cases where the two forms are equivalent, e.g. the one with square Cartesian product:
idinxpssinxp3 $p |- ( ( I i^i ( A X. A ) ) C_ ( R i^i ( A X. A ) ) <-> ( I |` A ) C_ R ) and
idinxpssinxp4 $p |- ( A. x e. A A. y e. A ( x = y -> x R y ) <-> A. x e. A x R x ) .
Cf. https://github.com/metamath/set.mm/pull/1286

A relation is converse/ly 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 ( ~ dfcnvrefrel3 ).

We use this new general concept to define two special but conventional concepts, disjoints and functions.

“Converse reflexivity” can only exist if the “standalone” definition of reflexivity is revealed (as opposed to the x R x type of definition which is “mixed” with and obscured by symmetry). I like the "naughtiness" of the concept ("what on earth could be the converse of reflexivity??"), its name is technically correct, and I stick to it:) Of course all proofs are welcome if this concept and a concept X are the same.
metamath/set.mm,metamath/set.mm,metamath/set.mm