Theorem petinidres2

Description: Class A is a partition by an intersection with the identity class restricted to it if and only if the cosets by the intersection are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021)

	Ref	Expression
Assertion	petinidres2	$$⊢\left(Disj\left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)\wedge \mathrm{dom}\left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)/\left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)=A\right)\leftrightarrow \left(EqvRel\wr \left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)\wedge \mathrm{dom}\wr \left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)/\wr \left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		disjALTVinidres	$$⊢Disj\left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)$$
2	1	petlemi	$$⊢\left(Disj\left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)\wedge \mathrm{dom}\left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)/\left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)=A\right)\leftrightarrow \left(EqvRel\wr \left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)\wedge \mathrm{dom}\wr \left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)/\wr \left(R\cap \left({\mathrm{I}\upharpoonright }_A\right)\right)=A\right)$$