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	$$⊢DisjR\leftrightarrow \left(FunALTV{R}^{-1}\wedge \mathrm{Rel}R\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-disjALTV	$$⊢DisjR\leftrightarrow \left(CnvRefRel\wr R^{-1}\wedge \mathrm{Rel}R\right)$$
2		relcnv	$$⊢\mathrm{Rel}{R}^{-1}$$
3		df-funALTV	$$⊢FunALTV{R}^{-1}\leftrightarrow \left(CnvRefRel\wr R^{-1}\wedge \mathrm{Rel}{R}^{-1}\right)$$
4	2 3	mpbiran2	$$⊢FunALTV{R}^{-1}\leftrightarrow CnvRefRel\wr R^{-1}$$
5	4	anbi1i	$$⊢\left(FunALTV{R}^{-1}\wedge \mathrm{Rel}R\right)\leftrightarrow \left(CnvRefRel\wr R^{-1}\wedge \mathrm{Rel}R\right)$$
6	1 5	bitr4i	$$⊢DisjR\leftrightarrow \left(FunALTV{R}^{-1}\wedge \mathrm{Rel}R\right)$$