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