This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mpofun

Description: The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012) (Proof shortened by SN, 23-Jul-2024)

Ref Expression
Hypothesis mpofun.1 
|- F = ( x e. A , y e. B |-> C )
Assertion mpofun 
|- Fun F

Proof

Step Hyp Ref Expression
1 mpofun.1 
 |-  F = ( x e. A , y e. B |-> C )
2 moeq 
 |-  E* z z = C
3 2 moani 
 |-  E* z ( ( x e. A /\ y e. B ) /\ z = C )
4 3 funoprab 
 |-  Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
5 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
6 1 5 eqtri 
 |-  F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
7 6 funeqi 
 |-  ( Fun F <-> Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } )
8 4 7 mpbir 
 |-  Fun F