Theorem partimeq

Description: Partition implies that the class of coelements on the natural domain is equal to the class of cosets of the relation, cf. erimeq . (Contributed by Peter Mazsa, 25-Dec-2024)

	Ref	Expression
Assertion	partimeq	Could not format assertion : No typesetting found for |- ( R e. V -> ( R Part A -> ~ A = ,~ R ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		cossex	$$⊢R\in V\to \wr R\in \mathrm{V}$$
2		partim	Could not format ( R Part A -> ,~ R ErALTV A ) : No typesetting found for |- ( R Part A -> ,~ R ErALTV A ) with typecode |-
3		erimeq	$$⊢\wr R\in \mathrm{V}\to \left(\wr RErALTVA\to \sim A=\wr R\right)$$
4	1 2 3	syl2im	Could not format ( R e. V -> ( R Part A -> ~ A = ,~ R ) ) : No typesetting found for |- ( R e. V -> ( R Part A -> ~ A = ,~ R ) ) with typecode |-