Theorem disjALTVid

Description: The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021)

	Ref	Expression
Assertion	disjALTVid	$$⊢Disj\mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		cosscnvid	$$⊢\wr {\mathrm{I}}^{-1}=\mathrm{I}$$
2	1	eqimssi	$$⊢\wr {\mathrm{I}}^{-1}\subseteq \mathrm{I}$$
3		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
4		dfdisjALTV2	$$⊢Disj\mathrm{I}\leftrightarrow \left(\wr {\mathrm{I}}^{-1}\subseteq \mathrm{I}\wedge \mathrm{Rel}\mathrm{I}\right)$$
5	2 3 4	mpbir2an	$$⊢Disj\mathrm{I}$$