elimampo

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

	Ref	Expression
Hypotheses	rngop.1	$⊢ F = (x \in A, y \in B ⟼ C)$
	elimampo.d	$⊢ φ \to D \in V$
	elimampo.x	$⊢ φ \to X \subseteq A$
	elimampo.y	$⊢ φ \to Y \subseteq B$
Assertion	elimampo	$⊢ φ \to (D \in F [X \times Y] \leftrightarrow \exists x \in X \exists y \in Y D = C)$

Step	Hyp	Ref	Expression
1		rngop.1	$⊢ F = (x \in A, y \in B ⟼ C)$
2		elimampo.d	$⊢ φ \to D \in V$
3		elimampo.x	$⊢ φ \to X \subseteq A$
4		elimampo.y	$⊢ φ \to Y \subseteq B$
5		df-ima	$⊢ F [X \times Y] = ran ({F ↾}_{(X \times Y)})$
6	5	eleq2i	$⊢ D \in F [X \times Y] \leftrightarrow D \in ran ({F ↾}_{(X \times Y)})$
7	1	reseq1i	$⊢ {F ↾}_{(X \times Y)} = {(x \in A, y \in B ⟼ C) ↾}_{(X \times Y)}$
8		resmpo	$⊢ (X \subseteq A \land Y \subseteq B) \to {(x \in A, y \in B ⟼ C) ↾}_{(X \times Y)} = (x \in X, y \in Y ⟼ C)$
9	3 4 8	syl2anc	$⊢ φ \to {(x \in A, y \in B ⟼ C) ↾}_{(X \times Y)} = (x \in X, y \in Y ⟼ C)$
10	7 9	eqtrid	$⊢ φ \to {F ↾}_{(X \times Y)} = (x \in X, y \in Y ⟼ C)$
11	10	rneqd	$⊢ φ \to ran ({F ↾}_{(X \times Y)}) = ran (x \in X, y \in Y ⟼ C)$
12	11	eleq2d	$⊢ φ \to (D \in ran ({F ↾}_{(X \times Y)}) \leftrightarrow D \in ran (x \in X, y \in Y ⟼ C))$
13	6 12	bitrid	$⊢ φ \to (D \in F [X \times Y] \leftrightarrow D \in ran (x \in X, y \in Y ⟼ C))$
14		eqid	$⊢ (x \in X, y \in Y ⟼ C) = (x \in X, y \in Y ⟼ C)$
15	14	elrnmpog	$⊢ D \in V \to (D \in ran (x \in X, y \in Y ⟼ C) \leftrightarrow \exists x \in X \exists y \in Y D = C)$
16	2 15	syl	$⊢ φ \to (D \in ran (x \in X, y \in Y ⟼ C) \leftrightarrow \exists x \in X \exists y \in Y D = C)$
17	13 16	bitrd	$⊢ φ \to (D \in F [X \times Y] \leftrightarrow \exists x \in X \exists y \in Y D = C)$

Metamath Proof Explorer