Definition df-disjs 39416

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 39425).

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

Assertion

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

Detailed syntax breakdown of Definition df-disjs

Step	Hyp	Ref	Expression
1		cdisjs 38845	. 2 class Disjs
2		cdisjss 38844	. . 3 class Disjss
3		crels 38812	. . 3 class Rels
4	2, 3	cin 3905	. 2 class ( Disjss ∩ Rels )
5	1, 4	wceq 1570	1 wff Disjs = ( Disjss ∩ Rels )

This definition is referenced by:  dfdisjs  39420  eldisjsim2  39562