Theorem cossex

Description: If A is a set then the class of cosets by A is a set. (Contributed by Peter Mazsa, 4-Jan-2019)

	Ref	Expression
Assertion	cossex	$$⊢A\in V\to \wr A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		dfcoss3	$$⊢\wr A=A\circ A^{-1}$$
2		cnvexg	$$⊢A\in V\to A^{-1}\in \mathrm{V}$$
3		coexg	$$⊢\left(A\in V\wedge A^{-1}\in \mathrm{V}\right)\to A\circ A^{-1}\in \mathrm{V}$$
4	2 3	mpdan	$$⊢A\in V\to A\circ A^{-1}\in \mathrm{V}$$
5	1 4	eqeltrid	$$⊢A\in V\to \wr A\in \mathrm{V}$$