Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-disjs | Structured version Visualization version GIF version |
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 36510).
The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 36524. Alternate definitions are dfdisjs 36505, ... , dfdisjs5 36509. (Contributed by Peter Mazsa, 17-Jul-2021.) |
Ref | Expression |
---|---|
df-disjs | ⊢ Disjs = ( Disjss ∩ Rels ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdisjs 36052 | . 2 class Disjs | |
2 | cdisjss 36051 | . . 3 class Disjss | |
3 | crels 36021 | . . 3 class Rels | |
4 | 2, 3 | cin 3852 | . 2 class ( Disjss ∩ Rels ) |
5 | 1, 4 | wceq 1543 | 1 wff Disjs = ( Disjss ∩ Rels ) |
Colors of variables: wff setvar class |
This definition is referenced by: dfdisjs 36505 |
Copyright terms: Public domain | W3C validator |