Metamath Proof Explorer

Theorem mpt3fvd

Description: Value of a three-argument function in maps-to notation. (Contributed by BTernaryTau, 28-Sep-2026)

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

Proof

Step Hyp Ref Expression
1 mpt3fvd.1 
 |-  ( ph -> X e. ( ( A X. B ) X. C ) )
2 mpt3fvd.2 
 |-  ( ph -> Y e. V )
3 mpt3fvd.3 
 |-  ( ( ph /\ X = <. x , y , z >. ) -> Y = D )
4 mpt3fvd.4 
 |-  F = ( x e. A , y e. B , z e. C |-> D )
5 el2xptp 
 |-  ( X e. ( ( A X. B ) X. C ) <-> E. x e. A E. y e. B E. z e. C X = <. x , y , z >. )
6 1 5 sylib 
 |-  ( ph -> E. x e. A E. y e. B E. z e. C X = <. x , y , z >. )
7 simpr 
 |-  ( ( ph /\ X = <. x , y , z >. ) -> X = <. x , y , z >. )
8 7 3 jca 
 |-  ( ( ph /\ X = <. x , y , z >. ) -> ( X = <. x , y , z >. /\ Y = D ) )
9 8 ex 
 |-  ( ph -> ( X = <. x , y , z >. -> ( X = <. x , y , z >. /\ Y = D ) ) )
10 9 reximdv 
 |-  ( ph -> ( E. z e. C X = <. x , y , z >. -> E. z e. C ( X = <. x , y , z >. /\ Y = D ) ) )
11 10 reximdv 
 |-  ( ph -> ( E. y e. B E. z e. C X = <. x , y , z >. -> E. y e. B E. z e. C ( X = <. x , y , z >. /\ Y = D ) ) )
12 11 reximdv 
 |-  ( ph -> ( E. x e. A E. y e. B E. z e. C X = <. x , y , z >. -> E. x e. A E. y e. B E. z e. C ( X = <. x , y , z >. /\ Y = D ) ) )
13 6 12 mpd 
 |-  ( ph -> E. x e. A E. y e. B E. z e. C ( X = <. x , y , z >. /\ Y = D ) )
14 1 elexd 
 |-  ( ph -> X e. _V )
15 eqeq1 
 |-  ( v = X -> ( v = <. x , y , z >. <-> X = <. x , y , z >. ) )
16 15 anbi1d 
 |-  ( v = X -> ( ( v = <. x , y , z >. /\ w = D ) <-> ( X = <. x , y , z >. /\ w = D ) ) )
17 16 rexbidv 
 |-  ( v = X -> ( E. z e. C ( v = <. x , y , z >. /\ w = D ) <-> E. z e. C ( X = <. x , y , z >. /\ w = D ) ) )
18 17 2rexbidv 
 |-  ( v = X -> ( E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) <-> E. x e. A E. y e. B E. z e. C ( X = <. x , y , z >. /\ w = D ) ) )
19 eqeq1 
 |-  ( w = Y -> ( w = D <-> Y = D ) )
20 19 anbi2d 
 |-  ( w = Y -> ( ( X = <. x , y , z >. /\ w = D ) <-> ( X = <. x , y , z >. /\ Y = D ) ) )
21 20 rexbidv 
 |-  ( w = Y -> ( E. z e. C ( X = <. x , y , z >. /\ w = D ) <-> E. z e. C ( X = <. x , y , z >. /\ Y = D ) ) )
22 21 2rexbidv 
 |-  ( w = Y -> ( E. x e. A E. y e. B E. z e. C ( X = <. x , y , z >. /\ w = D ) <-> E. x e. A E. y e. B E. z e. C ( X = <. x , y , z >. /\ Y = D ) ) )
23 moeq 
 |-  E* w w = D
24 23 moani 
 |-  E* w ( ( x e. A /\ y e. B /\ z e. C ) /\ w = D )
25 24 ax-gen 
 |-  A. z E* w ( ( x e. A /\ y e. B /\ z e. C ) /\ w = D )
26 25 gen2 
 |-  A. x A. y A. z E* w ( ( x e. A /\ y e. B /\ z e. C ) /\ w = D )
27 mosubott 
 |-  ( A. x A. y A. z E* w ( ( x e. A /\ y e. B /\ z e. C ) /\ w = D ) -> E* w E. x E. y E. z ( v = <. x , y , z >. /\ ( ( x e. A /\ y e. B /\ z e. C ) /\ w = D ) ) )
28 26 27 ax-mp 
 |-  E* w E. x E. y E. z ( v = <. x , y , z >. /\ ( ( x e. A /\ y e. B /\ z e. C ) /\ w = D ) )
29 r3ex 
 |-  ( E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) <-> E. x E. y E. z ( ( x e. A /\ y e. B /\ z e. C ) /\ ( v = <. x , y , z >. /\ w = D ) ) )
30 an12 
 |-  ( ( v = <. x , y , z >. /\ ( ( x e. A /\ y e. B /\ z e. C ) /\ w = D ) ) <-> ( ( x e. A /\ y e. B /\ z e. C ) /\ ( v = <. x , y , z >. /\ w = D ) ) )
31 30 3exbii 
 |-  ( E. x E. y E. z ( v = <. x , y , z >. /\ ( ( x e. A /\ y e. B /\ z e. C ) /\ w = D ) ) <-> E. x E. y E. z ( ( x e. A /\ y e. B /\ z e. C ) /\ ( v = <. x , y , z >. /\ w = D ) ) )
32 29 31 bitr4i 
 |-  ( E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) <-> E. x E. y E. z ( v = <. x , y , z >. /\ ( ( x e. A /\ y e. B /\ z e. C ) /\ w = D ) ) )
33 32 mobii 
 |-  ( E* w E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) <-> E* w E. x E. y E. z ( v = <. x , y , z >. /\ ( ( x e. A /\ y e. B /\ z e. C ) /\ w = D ) ) )
34 28 33 mpbir 
 |-  E* w E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D )
35 34 a1i 
 |-  ( v e. _V -> E* w E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) )
36 df-mpt3 
 |-  ( x e. A , y e. B , z e. C |-> D ) = { <. v , w >. | E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) }
37 vex 
 |-  v e. _V
38 37 biantrur 
 |-  ( E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) <-> ( v e. _V /\ E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) ) )
39 38 opabbii 
 |-  { <. v , w >. | E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) } = { <. v , w >. | ( v e. _V /\ E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) ) }
40 36 39 eqtri 
 |-  ( x e. A , y e. B , z e. C |-> D ) = { <. v , w >. | ( v e. _V /\ E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) ) }
41 18 22 35 40 fvopab3ig 
 |-  ( ( X e. _V /\ Y e. V ) -> ( E. x e. A E. y e. B E. z e. C ( X = <. x , y , z >. /\ Y = D ) -> ( ( x e. A , y e. B , z e. C |-> D ) ` X ) = Y ) )
42 4 fveq1i 
 |-  ( F ` X ) = ( ( x e. A , y e. B , z e. C |-> D ) ` X )
43 42 eqeq1i 
 |-  ( ( F ` X ) = Y <-> ( ( x e. A , y e. B , z e. C |-> D ) ` X ) = Y )
44 41 43 imbitrrdi 
 |-  ( ( X e. _V /\ Y e. V ) -> ( E. x e. A E. y e. B E. z e. C ( X = <. x , y , z >. /\ Y = D ) -> ( F ` X ) = Y ) )
45 14 2 44 syl2anc 
 |-  ( ph -> ( E. x e. A E. y e. B E. z e. C ( X = <. x , y , z >. /\ Y = D ) -> ( F ` X ) = Y ) )
46 13 45 mpd 
 |-  ( ph -> ( F ` X ) = Y )