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