Metamath Proof Explorer

Theorem funmpt3

Description: A function in maps-to notation with three arguments is a function. (Contributed by BTernaryTau, 8-Sep-2026)

Ref Expression
Assertion funmpt3 
|- Fun ( x e. A , y e. B , z e. C |-> D )

Proof

Step Hyp Ref Expression
1 funopab 
 |-  ( Fun { <. v , w >. | E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) } <-> A. v E* w E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) )
2 moeq 
 |-  E* w w = D
3 2 moani 
 |-  E* w ( ( x e. A /\ y e. B /\ z e. C ) /\ w = D )
4 3 ax-gen 
 |-  A. z E* w ( ( x e. A /\ y e. B /\ z e. C ) /\ w = D )
5 4 gen2 
 |-  A. x A. y A. z E* w ( ( x e. A /\ y e. B /\ z e. C ) /\ w = D )
6 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 ) ) )
7 5 6 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 ) )
8 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 ) ) )
9 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 ) ) )
10 9 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 ) ) )
11 8 10 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 ) ) )
12 11 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 ) ) )
13 7 12 mpbir 
 |-  E* w E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D )
14 1 13 mpgbir 
 |-  Fun { <. v , w >. | E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) }
15 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 ) }
16 15 funeqi 
 |-  ( Fun ( x e. A , y e. B , z e. C |-> D ) <-> Fun { <. v , w >. | E. x e. A E. y e. B E. z e. C ( v = <. x , y , z >. /\ w = D ) } )
17 14 16 mpbir 
 |-  Fun ( x e. A , y e. B , z e. C |-> D )