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 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | crels | ⊢ Rels | |
| 1 | cvv | ⊢ V | |
| 2 | 1 1 | cxp | ⊢ ( V × V ) |
| 3 | 2 | cpw | ⊢ 𝒫 ( V × V ) |
| 4 | 0 3 | wceq | ⊢ Rels = 𝒫 ( V × V ) |