Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rels Structured version   Visualization version   GIF version

Definition df-rels 34577
Description: Define the relations class. Proper class relations (like I, cf. reli 5387) are not elements of it. The element of this class and the relation predicate are the same when 𝑅 is a set (cf. elrelsrel 34579).

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 34602), 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 34577 (cf. df-refrels 34603 and the resulting dfrefrels2 34605 and dfrefrels3 34606).

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

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

Detailed syntax breakdown of Definition df-rels
StepHypRef Expression
1 crels 34317 . 2 class Rels
2 cvv 3351 . . . 4 class V
32, 2cxp 5248 . . 3 class (V × V)
43cpw 4298 . 2 class 𝒫 (V × V)
51, 4wceq 1631 1 wff Rels = 𝒫 (V × V)
Colors of variables: wff setvar class
This definition is referenced by:  elrels2  34578
  Copyright terms: Public domain W3C validator