Theorem mpofunOLD

Description: Obsolete version of mpofun as of 23-Jul-2024. (Contributed by Scott Fenton, 21-Mar-2012) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		mpofun.1	|- F = ( x e. A , y e. B |-> C )
2		eqtr3	|- ( ( z = C /\ w = C ) -> z = w )
3	2	ad2ant2l	|- ( ( ( ( x e. A /\ y e. B ) /\ z = C ) /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) -> z = w )
4	3	gen2	|- A. z A. w ( ( ( ( x e. A /\ y e. B ) /\ z = C ) /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) -> z = w )
5		eqeq1	|- ( z = w -> ( z = C <-> w = C ) )
6	5	anbi2d	|- ( z = w -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. A /\ y e. B ) /\ w = C ) ) )
7	6	mo4	|- ( E* z ( ( x e. A /\ y e. B ) /\ z = C ) <-> A. z A. w ( ( ( ( x e. A /\ y e. B ) /\ z = C ) /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) -> z = w ) )
8	4 7	mpbir	|- E* z ( ( x e. A /\ y e. B ) /\ z = C )
9	8	funoprab	|- Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
10		df-mpo	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
11	1 10	eqtri	|- F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
12	11	funeqi	|- ( Fun F <-> Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } )
13	9 12	mpbir	|- Fun F