Definition df-disjs

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

The element of the class of disjoints and the disjoint predicate are the same, that is ( R e. Disjs <-> Disj R ) when R is a set, see eldisjsdisj . Alternate definitions are dfdisjs , ... , dfdisjs5 . (Contributed by Peter Mazsa, 17-Jul-2021)

	Ref	Expression
Assertion	df-disjs	|- Disjs = ( Disjss i^i Rels )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdisjs	|- Disjs
1		cdisjss	|- Disjss
2		crels	|- Rels
3	1 2	cin	|- ( Disjss i^i Rels )
4	0 3	wceq	|- Disjs = ( Disjss i^i Rels )