Theorem relcoels

Description: Coelements on A is a relation. (Contributed by Peter Mazsa, 5-Oct-2021)

	Ref	Expression
Assertion	relcoels	$$⊢\mathrm{Rel}\sim A$$

Proof

Step	Hyp	Ref	Expression
1		relcoss	$$⊢\mathrm{Rel}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
2		df-coels	$$⊢\sim A=\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
3	2	releqi	$$⊢\mathrm{Rel}\sim A\leftrightarrow \mathrm{Rel}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
4	1 3	mpbir	$$⊢\mathrm{Rel}\sim A$$