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	|- ( ( A e. V \/ ( ( A |` B ) e. W /\ B e. X ) ) -> ( A " B ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		imassrn	|- ( A " B ) C_ ran A
2		rnexg	|- ( A e. V -> ran A e. _V )
3		ssexg	|- ( ( ( A " B ) C_ ran A /\ ran A e. _V ) -> ( A " B ) e. _V )
4	1 2 3	sylancr	|- ( A e. V -> ( A " B ) e. _V )
5		qsexg	|- ( B e. X -> ( B /. A ) e. _V )
6		uniexg	|- ( ( B /. A ) e. _V -> U. ( B /. A ) e. _V )
7	5 6	syl	|- ( B e. X -> U. ( B /. A ) e. _V )
8		uniqsALTV	|- ( ( A |` B ) e. W -> U. ( B /. A ) = ( A " B ) )
9	8	eleq1d	|- ( ( A |` B ) e. W -> ( U. ( B /. A ) e. _V <-> ( A " B ) e. _V ) )
10	7 9	syl5ib	|- ( ( A |` B ) e. W -> ( B e. X -> ( A " B ) e. _V ) )
11	10	imp	|- ( ( ( A |` B ) e. W /\ B e. X ) -> ( A " B ) e. _V )
12	4 11	jaoi	|- ( ( A e. V \/ ( ( A |` B ) e. W /\ B e. X ) ) -> ( A " B ) e. _V )