Metamath Proof Explorer


Definition df-rels

Description: Define the relations class. Proper class relations (like _I , see reli ) are not elements of it. The element of this class and the relation predicate are the same when R is a set (see elrelsrel ).

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 . 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 ), 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 (see df-refrels and the resulting dfrefrels2 and dfrefrels3 ).

3. Finally, in order to be able to work with proper classes (like iprc ) as well, we define the predicate of the relation (see df-refrel ) so that it is true for the relevant proper classes (see refrelid ), and that the element of the class of the required relations (e.g. elrefrels3 ) and this predicate are the same in case of sets (see elrefrelsrel ). (Contributed by Peter Mazsa, 13-Jun-2018)

Ref Expression
Assertion df-rels Rels = 𝒫 V × V

Detailed syntax breakdown

Step Hyp Ref Expression
0 crels class Rels
1 cvv class V
2 1 1 cxp class V × V
3 2 cpw class 𝒫 V × V
4 0 3 wceq wff Rels = 𝒫 V × V