Theorem elimampo

Description: Membership in the image of an operation. (Contributed by SN, 27-Apr-2025)

	Ref	Expression
Hypotheses	rngop.1	|- F = ( x e. A , y e. B |-> C )
	elimampo.d	|- ( ph -> D e. V )
	elimampo.x	|- ( ph -> X C_ A )
	elimampo.y	|- ( ph -> Y C_ B )
Assertion	elimampo	|- ( ph -> ( D e. ( F " ( X X. Y ) ) <-> E. x e. X E. y e. Y D = C ) )

Proof

Step	Hyp	Ref	Expression
1		rngop.1	|- F = ( x e. A , y e. B |-> C )
2		elimampo.d	|- ( ph -> D e. V )
3		elimampo.x	|- ( ph -> X C_ A )
4		elimampo.y	|- ( ph -> Y C_ B )
5		df-ima	|- ( F " ( X X. Y ) ) = ran ( F |` ( X X. Y ) )
6	5	eleq2i	|- ( D e. ( F " ( X X. Y ) ) <-> D e. ran ( F |` ( X X. Y ) ) )
7	1	reseq1i	|- ( F |` ( X X. Y ) ) = ( ( x e. A , y e. B |-> C ) |` ( X X. Y ) )
8		resmpo	|- ( ( X C_ A /\ Y C_ B ) -> ( ( x e. A , y e. B |-> C ) |` ( X X. Y ) ) = ( x e. X , y e. Y |-> C ) )
9	3 4 8	syl2anc	|- ( ph -> ( ( x e. A , y e. B |-> C ) |` ( X X. Y ) ) = ( x e. X , y e. Y |-> C ) )
10	7 9	eqtrid	|- ( ph -> ( F |` ( X X. Y ) ) = ( x e. X , y e. Y |-> C ) )
11	10	rneqd	|- ( ph -> ran ( F |` ( X X. Y ) ) = ran ( x e. X , y e. Y |-> C ) )
12	11	eleq2d	|- ( ph -> ( D e. ran ( F |` ( X X. Y ) ) <-> D e. ran ( x e. X , y e. Y |-> C ) ) )
13	6 12	bitrid	|- ( ph -> ( D e. ( F " ( X X. Y ) ) <-> D e. ran ( x e. X , y e. Y |-> C ) ) )
14		eqid	|- ( x e. X , y e. Y |-> C ) = ( x e. X , y e. Y |-> C )
15	14	elrnmpog	|- ( D e. V -> ( D e. ran ( x e. X , y e. Y |-> C ) <-> E. x e. X E. y e. Y D = C ) )
16	2 15	syl	|- ( ph -> ( D e. ran ( x e. X , y e. Y |-> C ) <-> E. x e. X E. y e. Y D = C ) )
17	13 16	bitrd	|- ( ph -> ( D e. ( F " ( X X. Y ) ) <-> E. x e. X E. y e. Y D = C ) )