Theorem cnvepimaex

Description: The image of converse epsilon exists, proof via imaexALTV (see also cnvepima and uniexg for alternate way). (Contributed by Peter Mazsa, 22-Mar-2023)

	Ref	Expression
Assertion	cnvepimaex	$$⊢A\in V\to {\mathrm{E}}^{-1}\left[A\right]\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		cnvepresex	$$⊢A\in V\to {{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{V}$$
2		imaexALTV	$$⊢\left({\mathrm{E}}^{-1}\in \mathrm{V}\vee \left({{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{V}\wedge A\in V\right)\right)\to {\mathrm{E}}^{-1}\left[A\right]\in \mathrm{V}$$
3	2	olcs	$$⊢\left({{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{V}\wedge A\in V\right)\to {\mathrm{E}}^{-1}\left[A\right]\in \mathrm{V}$$
4	1 3	mpancom	$$⊢A\in V\to {\mathrm{E}}^{-1}\left[A\right]\in \mathrm{V}$$