Theorem elimampo

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

	Ref	Expression
Hypotheses	rngop.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
	elimampo.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	elimampo.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝐴 )
	elimampo.y	⊢ ( 𝜑 → 𝑌 ⊆ 𝐵 )
Assertion	elimampo	⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝐹 “ ( 𝑋 × 𝑌 ) ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝐷 = 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		rngop.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2		elimampo.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3		elimampo.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝐴 )
4		elimampo.y	⊢ ( 𝜑 → 𝑌 ⊆ 𝐵 )
5		df-ima	⊢ ( 𝐹 “ ( 𝑋 × 𝑌 ) ) = ran ( 𝐹 ↾ ( 𝑋 × 𝑌 ) )
6	5	eleq2i	⊢ ( 𝐷 ∈ ( 𝐹 “ ( 𝑋 × 𝑌 ) ) ↔ 𝐷 ∈ ran ( 𝐹 ↾ ( 𝑋 × 𝑌 ) ) )
7	1	reseq1i	⊢ ( 𝐹 ↾ ( 𝑋 × 𝑌 ) ) = ( ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ↾ ( 𝑋 × 𝑌 ) )
8		resmpo	⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ↾ ( 𝑋 × 𝑌 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) )
9	3 4 8	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ↾ ( 𝑋 × 𝑌 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) )
10	7 9	eqtrid	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 × 𝑌 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) )
11	10	rneqd	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( 𝑋 × 𝑌 ) ) = ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) )
12	11	eleq2d	⊢ ( 𝜑 → ( 𝐷 ∈ ran ( 𝐹 ↾ ( 𝑋 × 𝑌 ) ) ↔ 𝐷 ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) )
13	6 12	bitrid	⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝐹 “ ( 𝑋 × 𝑌 ) ) ↔ 𝐷 ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) )
14		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 )
15	14	elrnmpog	⊢ ( 𝐷 ∈ 𝑉 → ( 𝐷 ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝐷 = 𝐶 ) )
16	2 15	syl	⊢ ( 𝜑 → ( 𝐷 ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝐷 = 𝐶 ) )
17	13 16	bitrd	⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝐹 “ ( 𝑋 × 𝑌 ) ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝐷 = 𝐶 ) )