Theorem dfeldisj2

Description: Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021)

	Ref	Expression
Assertion	dfeldisj2	$$⊢ElDisjA\leftrightarrow \wr {\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)}^{-1}\subseteq \mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		df-eldisj	$$⊢ElDisjA\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
2		relres	$$⊢\mathrm{Rel}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
3		dfdisjALTV2	$$⊢Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\leftrightarrow \left(\wr {\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)}^{-1}\subseteq \mathrm{I}\wedge \mathrm{Rel}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\right)$$
4	2 3	mpbiran2	$$⊢Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\leftrightarrow \wr {\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)}^{-1}\subseteq \mathrm{I}$$
5	1 4	bitri	$$⊢ElDisjA\leftrightarrow \wr {\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)}^{-1}\subseteq \mathrm{I}$$