Theorem 1cossxrncnvepresex

Description: Sufficient condition for a restricted converse epsilon range Cartesian product to be a set. (Contributed by Peter Mazsa, 23-Sep-2021)

	Ref	Expression
Assertion	1cossxrncnvepresex	$$⊢\left(A\in V\wedge R\in W\right)\to \wr R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		xrncnvepresex	$$⊢\left(A\in V\wedge R\in W\right)\to R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\in \mathrm{V}$$
2		cossex	$$⊢R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\in \mathrm{V}\to \wr R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\in \mathrm{V}$$
3	1 2	syl	$$⊢\left(A\in V\wedge R\in W\right)\to \wr R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\in \mathrm{V}$$