Description: Alternate definition of the disjoint relation predicate. A disjoint relation is a converse function of the relation, see the comment of df-disjs why we need disjoint relations instead of converse functions anyway. (Contributed by Peter Mazsa, 27-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfdisjALTV | |- ( Disj R <-> ( FunALTV `' R /\ Rel R ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-disjALTV | |- ( Disj R <-> ( CnvRefRel ,~ `' R /\ Rel R ) ) |
|
| 2 | relcnv | |- Rel `' R |
|
| 3 | df-funALTV | |- ( FunALTV `' R <-> ( CnvRefRel ,~ `' R /\ Rel `' R ) ) |
|
| 4 | 2 3 | mpbiran2 | |- ( FunALTV `' R <-> CnvRefRel ,~ `' R ) |
| 5 | 4 | anbi1i | |- ( ( FunALTV `' R /\ Rel R ) <-> ( CnvRefRel ,~ `' R /\ Rel R ) ) |
| 6 | 1 5 | bitr4i | |- ( Disj R <-> ( FunALTV `' R /\ Rel R ) ) |