This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝐹 “ ( 𝑋 × 𝑌 ) ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝐷 = 𝐶 ) )