Metamath Proof Explorer

Theorem elimampo

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

Ref Expression
Hypotheses rngop.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
elimampo.d ⊢ φ → D ∈ V
elimampo.x ⊢ φ → X ⊆ A
elimampo.y ⊢ φ → Y ⊆ B
Assertion elimampo ⊢ φ → D ∈ F X × Y ↔ ∃ x ∈ X ∃ y ∈ Y D = C

Proof

Step Hyp Ref Expression
1 rngop.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
2 elimampo.d ⊢ φ → D ∈ V
3 elimampo.x ⊢ φ → X ⊆ A
4 elimampo.y ⊢ φ → Y ⊆ B
5 df-ima ⊢ F X × Y = ran ⁡ F ↾ X × Y
6 5 eleq2i ⊢ D ∈ F X × Y ↔ D ∈ ran ⁡ F ↾ X × Y
7 1 reseq1i ⊢ F ↾ X × Y = x ∈ A , y ∈ B ⟼ C ↾ X × Y
8 resmpo ⊢ X ⊆ A ∧ Y ⊆ B → x ∈ A , y ∈ B ⟼ C ↾ X × Y = x ∈ X , y ∈ Y ⟼ C
9 3 4 8 syl2anc ⊢ φ → x ∈ A , y ∈ B ⟼ C ↾ X × Y = x ∈ X , y ∈ Y ⟼ C
10 7 9 eqtrid ⊢ φ → F ↾ X × Y = x ∈ X , y ∈ Y ⟼ C
11 10 rneqd ⊢ φ → ran ⁡ F ↾ X × Y = ran ⁡ x ∈ X , y ∈ Y ⟼ C
12 11 eleq2d ⊢ φ → D ∈ ran ⁡ F ↾ X × Y ↔ D ∈ ran ⁡ x ∈ X , y ∈ Y ⟼ C
13 6 12 bitrid ⊢ φ → D ∈ F X × Y ↔ D ∈ ran ⁡ x ∈ X , y ∈ Y ⟼ C
14 eqid ⊢ x ∈ X , y ∈ Y ⟼ C = x ∈ X , y ∈ Y ⟼ C
15 14 elrnmpog ⊢ D ∈ V → D ∈ ran ⁡ x ∈ X , y ∈ Y ⟼ C ↔ ∃ x ∈ X ∃ y ∈ Y D = C
16 2 15 syl ⊢ φ → D ∈ ran ⁡ x ∈ X , y ∈ Y ⟼ C ↔ ∃ x ∈ X ∃ y ∈ Y D = C
17 13 16 bitrd ⊢ φ → D ∈ F X × Y ↔ ∃ x ∈ X ∃ y ∈ Y D = C