Definition df-rels 34847

Description: Define the relations class. Proper class relations (like I, cf. reli 5495) are not elements of it. The element of this class and the relation predicate are the same when 𝑅 is a set (cf. elrelsrel 34849).

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 http://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 (cf. e.g. df-refs 34872), 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 34847 (cf. df-refrels 34873 and the resulting dfrefrels2 34875 and dfrefrels3 34876).

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

Assertion

Ref	Expression
df-rels	⊢ Rels = 𝒫 (V × V)

Detailed syntax breakdown of Definition df-rels

Step	Hyp	Ref	Expression
1		crels 34592	. 2 class Rels
2		cvv 3397	. . . 4 class V
3	2, 2	cxp 5353	. . 3 class (V × V)
4	3	cpw 4378	. 2 class 𝒫 (V × V)
5	1, 4	wceq 1601	1 wff Rels = 𝒫 (V × V)

This definition is referenced by:  elrels2  34848