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