Description: Define the disjoint relation predicate, i.e., the disjoint predicate. A disjoint relation is a converse function of the relation by dfdisjALTV , see the comment of df-disjs why we need disjoint relations instead of converse functions anyway.
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 dfdisjALTV , ... , dfdisjALTV5 . (Contributed by Peter Mazsa, 17-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-disjALTV | |- ( Disj R <-> ( CnvRefRel ,~ `' R /\ Rel R ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cR | |- R |
|
| 1 | 0 | wdisjALTV | |- Disj R |
| 2 | 0 | ccnv | |- `' R |
| 3 | 2 | ccoss | |- ,~ `' R |
| 4 | 3 | wcnvrefrel | |- CnvRefRel ,~ `' R |
| 5 | 0 | wrel | |- Rel R |
| 6 | 4 5 | wa | |- ( CnvRefRel ,~ `' R /\ Rel R ) |
| 7 | 1 6 | wb | |- ( Disj R <-> ( CnvRefRel ,~ `' R /\ Rel R ) ) |