Metamath Proof Explorer

Theorem mpofvd

Description: Value of a two-argument function (usually an operation) in maps-to notation. (Contributed by BTernaryTau, 18-Oct-2026)

Ref Expression
Hypotheses mpofvd.1 
|- ( ph -> X e. ( A X. B ) )
mpofvd.2 
|- ( ph -> Y e. V )
mpofvd.3 
|- ( ( ph /\ X = <. x , y >. ) -> Y = C )
mpofvd.4 
|- F = ( x e. A , y e. B |-> C )
Assertion mpofvd 
|- ( ph -> ( F ` X ) = Y )

Proof

Step Hyp Ref Expression
1 mpofvd.1 
 |-  ( ph -> X e. ( A X. B ) )
2 mpofvd.2 
 |-  ( ph -> Y e. V )
3 mpofvd.3 
 |-  ( ( ph /\ X = <. x , y >. ) -> Y = C )
4 mpofvd.4 
 |-  F = ( x e. A , y e. B |-> C )
5 elxpi 
 |-  ( X e. ( A X. B ) -> E. x E. y ( X = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
6 1 5 syl 
 |-  ( ph -> E. x E. y ( X = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
7 idd 
 |-  ( ( ph /\ X = <. x , y >. ) -> ( ( x e. A /\ y e. B ) -> ( x e. A /\ y e. B ) ) )
8 7 3 jctird 
 |-  ( ( ph /\ X = <. x , y >. ) -> ( ( x e. A /\ y e. B ) -> ( ( x e. A /\ y e. B ) /\ Y = C ) ) )
9 8 imdistanda 
 |-  ( ph -> ( ( X = <. x , y >. /\ ( x e. A /\ y e. B ) ) -> ( X = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ Y = C ) ) ) )
10 9 2eximdv 
 |-  ( ph -> ( E. x E. y ( X = <. x , y >. /\ ( x e. A /\ y e. B ) ) -> E. x E. y ( X = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ Y = C ) ) ) )
11 6 10 mpd 
 |-  ( ph -> E. x E. y ( X = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ Y = C ) ) )
12 1 elexd 
 |-  ( ph -> X e. _V )
13 eqeq1 
 |-  ( w = X -> ( w = <. x , y >. <-> X = <. x , y >. ) )
14 13 anbi1d 
 |-  ( w = X -> ( ( w = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) <-> ( X = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) )
15 14 2exbidv 
 |-  ( w = X -> ( E. x E. y ( w = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) <-> E. x E. y ( X = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) )
16 eqeq1 
 |-  ( z = Y -> ( z = C <-> Y = C ) )
17 16 anbi2d 
 |-  ( z = Y -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. A /\ y e. B ) /\ Y = C ) ) )
18 17 anbi2d 
 |-  ( z = Y -> ( ( X = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) <-> ( X = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ Y = C ) ) ) )
19 18 2exbidv 
 |-  ( z = Y -> ( E. x E. y ( X = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) <-> E. x E. y ( X = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ Y = C ) ) ) )
20 moeq 
 |-  E* z z = C
21 20 moani 
 |-  E* z ( ( x e. A /\ y e. B ) /\ z = C )
22 21 mosubop 
 |-  E* z E. x E. y ( w = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) )
23 22 a1i 
 |-  ( w e. _V -> E* z E. x E. y ( w = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) )
24 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
25 dfoprab2 
 |-  { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) }
26 4 24 25 3eqtri 
 |-  F = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) }
27 vex 
 |-  w e. _V
28 27 biantrur 
 |-  ( E. x E. y ( w = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) <-> ( w e. _V /\ E. x E. y ( w = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) )
29 28 opabbii 
 |-  { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) } = { <. w , z >. | ( w e. _V /\ E. x E. y ( w = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) }
30 26 29 eqtri 
 |-  F = { <. w , z >. | ( w e. _V /\ E. x E. y ( w = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) }
31 15 19 23 30 fvopab3ig 
 |-  ( ( X e. _V /\ Y e. V ) -> ( E. x E. y ( X = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ Y = C ) ) -> ( F ` X ) = Y ) )
32 12 2 31 syl2anc 
 |-  ( ph -> ( E. x E. y ( X = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ Y = C ) ) -> ( F ` X ) = Y ) )
33 11 32 mpd 
 |-  ( ph -> ( F ` X ) = Y )