**Description: **Define the relations
class. Proper class relations (like I, see
reli 5674) are not elements of it. The element of this
class and the
relation predicate are the same when 𝑅 is a set (see elrelsrel 35763).
The class of relations is a great tool we can use when we define classes
of different relations as nullary class constants as required by the 2.
point in our Guidelines https://us.metamath.org/mpeuni/mathbox.html 35763.
When we want to define a specific class of relations as a nullary class
constant, the appropriate method is the following:
1. We define the specific nullary class constant for general sets (see
e.g. df-refs 35786), then
2. we get the required class of relations by the intersection of the class
of general sets above with the class of relations df-rels 35761 (see
df-refrels 35787 and the resulting dfrefrels2 35789 and dfrefrels3 35790).
3. Finally, in order to be able to work with proper classes (like
iprc 7596) as well, we define the predicate of the
relation (see
df-refrel 35788) so that it is true for the relevant proper
classes (see
refrelid 35797), and that the element of the class of the
required relations
(e.g. elrefrels3 35794) and this predicate are the same in case of
sets (see
elrefrelsrel 35795). (Contributed by Peter Mazsa,
13-Jun-2018.) |