| Description: Define a general binary
relation. Note that the syntax is simply three
class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29
generalized to arbitrary classes. Class 𝑅 often denotes a relation
such as "< " that compares two
classes 𝐴 and 𝐵, which might
be numbers such as 1 and 2
(see df-ltxr 11154 for the specific
definition of <). As a wff, relations are true
or false. For
example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩}
→ 3𝑅9) (ex-br 30375).
Often class 𝑅 meets the Rel criteria to be defined in df-rel 5626,
and in particular 𝑅 may be a function (see df-fun 6484). This
definition of relations is well-defined, although not very meaningful,
when classes 𝐴 and/or 𝐵 are proper classes
(i.e., are not sets).
On the other hand, we often find uses for this definition when 𝑅 is a
proper class (see for example iprc 7844). (Contributed by NM,
31-Dec-1993.) |
