Theorem imaexALTV

Description: Existence of an image of a class. Theorem 3.17 of Monk1 p. 39. (cf. imaexg ) with weakened antecedent: only the restricion of A by a set needs to be a set, not A itself, see e.g. cnvepimaex . (Contributed by Peter Mazsa, 22-Feb-2023) (Proof modification is discouraged.)

	Ref	Expression
Assertion	imaexALTV	$$⊢\left(A\in V\vee \left({A\upharpoonright }_B\in W\wedge B\in X\right)\right)\to A\left[B\right]\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		imassrn	$$⊢A\left[B\right]\subseteq \mathrm{ran}A$$
2		rnexg	$$⊢A\in V\to \mathrm{ran}A\in \mathrm{V}$$
3		ssexg	$$⊢\left(A\left[B\right]\subseteq \mathrm{ran}A\wedge \mathrm{ran}A\in \mathrm{V}\right)\to A\left[B\right]\in \mathrm{V}$$
4	1 2 3	sylancr	$$⊢A\in V\to A\left[B\right]\in \mathrm{V}$$
5		qsexg	$$⊢B\in X\to B/A\in \mathrm{V}$$
6		uniexg	$$⊢B/A\in \mathrm{V}\to \bigcup \left(B/A\right)\in \mathrm{V}$$
7	5 6	syl	$$⊢B\in X\to \bigcup \left(B/A\right)\in \mathrm{V}$$
8		uniqsALTV	$$⊢{A\upharpoonright }_B\in W\to \bigcup \left(B/A\right)=A\left[B\right]$$
9	8	eleq1d	$$⊢{A\upharpoonright }_B\in W\to \left(\bigcup \left(B/A\right)\in \mathrm{V}\leftrightarrow A\left[B\right]\in \mathrm{V}\right)$$
10	7 9	syl5ib	$$⊢{A\upharpoonright }_B\in W\to \left(B\in X\to A\left[B\right]\in \mathrm{V}\right)$$
11	10	imp	$$⊢\left({A\upharpoonright }_B\in W\wedge B\in X\right)\to A\left[B\right]\in \mathrm{V}$$
12	4 11	jaoi	$$⊢\left(A\in V\vee \left({A\upharpoonright }_B\in W\wedge B\in X\right)\right)\to A\left[B\right]\in \mathrm{V}$$