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

Definition df-disjs 37212
Description: Define the disjoint relations class, i.e., the class of disjoints. We need Disjs for the definition of Parts and Part for the Partition-Equivalence Theorems: this need for Parts as disjoint relations on their domain quotients is the reason why we must define Disjs instead of simply using converse functions (cf. dfdisjALTV 37221).

The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 37235. Alternate definitions are dfdisjs 37216, ... , dfdisjs5 37220. (Contributed by Peter Mazsa, 17-Jul-2021.)

Assertion
Ref Expression
df-disjs Disjs = ( Disjss ∩ Rels )

Detailed syntax breakdown of Definition df-disjs
StepHypRef Expression
1 cdisjs 36713 . 2 class Disjs
2 cdisjss 36712 . . 3 class Disjss
3 crels 36682 . . 3 class Rels
42, 3cin 3910 . 2 class ( Disjss ∩ Rels )
51, 4wceq 1542 1 wff Disjs = ( Disjss ∩ Rels )
Colors of variables: wff setvar class
This definition is referenced by:  dfdisjs  37216
  Copyright terms: Public domain W3C validator