Theorem eldisjs

Description: Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 24-Jul-2021)

	Ref	Expression
Assertion	eldisjs	$$⊢R\in \mathrm{Disjs}\leftrightarrow \left(\wr R^{-1}\in \mathrm{CnvRefRels}\wedge R\in \mathrm{Rels}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfdisjs	$$⊢\mathrm{Disjs}=\left\{r\in \mathrm{Rels}|\wr r^{-1}\in \mathrm{CnvRefRels}\right\}$$
2		cnveq	$$⊢r=R\to r^{-1}=R^{-1}$$
3	2	cosseqd	$$⊢r=R\to \wr r^{-1}=\wr R^{-1}$$
4	3	eleq1d	$$⊢r=R\to \left(\wr r^{-1}\in \mathrm{CnvRefRels}\leftrightarrow \wr R^{-1}\in \mathrm{CnvRefRels}\right)$$
5	1 4	rabeqel	$$⊢R\in \mathrm{Disjs}\leftrightarrow \left(\wr R^{-1}\in \mathrm{CnvRefRels}\wedge R\in \mathrm{Rels}\right)$$