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		cosselcnvrefrels2	$$⊢\wr r^{-1}\in \mathrm{CnvRefRels}\leftrightarrow \left(\wr r^{-1}\subseteq \mathrm{I}\wedge \wr r^{-1}\in \mathrm{Rels}\right)$$
3		cosscnvelrels	$$⊢r\in \mathrm{Rels}\to \wr r^{-1}\in \mathrm{Rels}$$
4	3	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)$$
5	2 4	bitr4id	$$⊢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\}$$