Theorem dfdisjs2

Description: Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021)

	Ref	Expression
Assertion	dfdisjs2	$$⊢\mathrm{Disjs}=\left\{r\in \mathrm{Rels}|\wr r^{-1}\subseteq \mathrm{I}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfdisjs	$$⊢\mathrm{Disjs}=\left\{r\in \mathrm{Rels}|\wr r^{-1}\in \mathrm{CnvRefRels}\right\}$$
2		cosscnvelrels	$$⊢r\in \mathrm{Rels}\to \wr r^{-1}\in \mathrm{Rels}$$
3	2	biantrud	$$⊢r\in \mathrm{Rels}\to \left(\wr r^{-1}\subseteq \mathrm{I}\leftrightarrow \left(\wr r^{-1}\subseteq \mathrm{I}\wedge \wr r^{-1}\in \mathrm{Rels}\right)\right)$$
4		cosselcnvrefrels2	$$⊢\wr r^{-1}\in \mathrm{CnvRefRels}\leftrightarrow \left(\wr r^{-1}\subseteq \mathrm{I}\wedge \wr r^{-1}\in \mathrm{Rels}\right)$$
5	3 4	syl6rbbr	$$⊢r\in \mathrm{Rels}\to \left(\wr r^{-1}\in \mathrm{CnvRefRels}\leftrightarrow \wr r^{-1}\subseteq \mathrm{I}\right)$$
6	1 5	rabimbieq	$$⊢\mathrm{Disjs}=\left\{r\in \mathrm{Rels}|\wr r^{-1}\subseteq \mathrm{I}\right\}$$