Definition df-disjALTV

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1	0	wdisjALTV	$$wffDisjR$$
2	0	ccnv	$$class{R}^{-1}$$
3	2	ccoss	$$class\wr R^{-1}$$
4	3	wcnvrefrel	$$wffCnvRefRel\wr R^{-1}$$
5	0	wrel	$$wff\mathrm{Rel}R$$
6	4 5	wa	$$wff\left(CnvRefRel\wr R^{-1}\wedge \mathrm{Rel}R\right)$$
7	1 6	wb	$$wff\left(DisjR\leftrightarrow \left(CnvRefRel\wr R^{-1}\wedge \mathrm{Rel}R\right)\right)$$