Metamath Proof Explorer


Theorem dfdisjALTV

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

Proof

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