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 
|- F = ( x e. A , y e. B |-> C )
elimampo.d 
|- ( ph -> D e. V )
elimampo.x 
|- ( ph -> X C_ A )
elimampo.y 
|- ( ph -> Y C_ B )
Assertion elimampo 
|- ( ph -> ( D e. ( F " ( X X. Y ) ) <-> E. x e. X E. y e. Y D = C ) )

Proof

Step Hyp Ref Expression
1 rngop.1 
 |-  F = ( x e. A , y e. B |-> C )
2 elimampo.d 
 |-  ( ph -> D e. V )
3 elimampo.x 
 |-  ( ph -> X C_ A )
4 elimampo.y 
 |-  ( ph -> Y C_ B )
5 df-ima 
 |-  ( F " ( X X. Y ) ) = ran ( F |` ( X X. Y ) )
6 5 eleq2i 
 |-  ( D e. ( F " ( X X. Y ) ) <-> D e. ran ( F |` ( X X. Y ) ) )
7 1 reseq1i 
 |-  ( F |` ( X X. Y ) ) = ( ( x e. A , y e. B |-> C ) |` ( X X. Y ) )
8 resmpo 
 |-  ( ( X C_ A /\ Y C_ B ) -> ( ( x e. A , y e. B |-> C ) |` ( X X. Y ) ) = ( x e. X , y e. Y |-> C ) )
9 3 4 8 syl2anc 
 |-  ( ph -> ( ( x e. A , y e. B |-> C ) |` ( X X. Y ) ) = ( x e. X , y e. Y |-> C ) )
10 7 9 eqtrid 
 |-  ( ph -> ( F |` ( X X. Y ) ) = ( x e. X , y e. Y |-> C ) )
11 10 rneqd 
 |-  ( ph -> ran ( F |` ( X X. Y ) ) = ran ( x e. X , y e. Y |-> C ) )
12 11 eleq2d 
 |-  ( ph -> ( D e. ran ( F |` ( X X. Y ) ) <-> D e. ran ( x e. X , y e. Y |-> C ) ) )
13 6 12 bitrid 
 |-  ( ph -> ( D e. ( F " ( X X. Y ) ) <-> D e. ran ( x e. X , y e. Y |-> C ) ) )
14 eqid 
 |-  ( x e. X , y e. Y |-> C ) = ( x e. X , y e. Y |-> C )
15 14 elrnmpog 
 |-  ( D e. V -> ( D e. ran ( x e. X , y e. Y |-> C ) <-> E. x e. X E. y e. Y D = C ) )
16 2 15 syl 
 |-  ( ph -> ( D e. ran ( x e. X , y e. Y |-> C ) <-> E. x e. X E. y e. Y D = C ) )
17 13 16 bitrd 
 |-  ( ph -> ( D e. ( F " ( X X. Y ) ) <-> E. x e. X E. y e. Y D = C ) )