Theorem dfdisjALTV2

Description: Alternate definition of the disjoint relation predicate, cf. dffunALTV2 . (Contributed by Peter Mazsa, 27-Jul-2021)

	Ref	Expression
Assertion	dfdisjALTV2	$$⊢DisjR\leftrightarrow \left(\wr R^{-1}\subseteq \mathrm{I}\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		cnvrefrelcoss2	$$⊢CnvRefRel\wr R^{-1}\leftrightarrow \wr R^{-1}\subseteq \mathrm{I}$$
3	2	anbi1i	$$⊢\left(CnvRefRel\wr R^{-1}\wedge \mathrm{Rel}R\right)\leftrightarrow \left(\wr R^{-1}\subseteq \mathrm{I}\wedge \mathrm{Rel}R\right)$$
4	1 3	bitri	$$⊢DisjR\leftrightarrow \left(\wr R^{-1}\subseteq \mathrm{I}\wedge \mathrm{Rel}R\right)$$