Theorem setrec2lem2

Description: Lemma for setrec2 . The functional part of F is a function. (Contributed by Emmett Weisz, 6-Mar-2021) (New usage is discouraged.)

	Ref	Expression
Assertion	setrec2lem2	|- Fun ( F |` { x | E! y x F y } )

Proof

Step	Hyp	Ref	Expression
1		relres	|- Rel ( F |` { x | E! y x F y } )
2		fvex	|- ( F ` x ) e. _V
3		eqeq2	|- ( z = ( F ` x ) -> ( y = z <-> y = ( F ` x ) ) )
4	3	imbi2d	|- ( z = ( F ` x ) -> ( ( x ( F |` { x | E! y x F y } ) y -> y = z ) <-> ( x ( F |` { x | E! y x F y } ) y -> y = ( F ` x ) ) ) )
5	4	albidv	|- ( z = ( F ` x ) -> ( A. y ( x ( F |` { x | E! y x F y } ) y -> y = z ) <-> A. y ( x ( F |` { x | E! y x F y } ) y -> y = ( F ` x ) ) ) )
6	2 5	spcev	|- ( A. y ( x ( F |` { x | E! y x F y } ) y -> y = ( F ` x ) ) -> E. z A. y ( x ( F |` { x | E! y x F y } ) y -> y = z ) )
7		vex	|- y e. _V
8	7	brresi	|- ( x ( F |` { x | E! y x F y } ) y <-> ( x e. { x | E! y x F y } /\ x F y ) )
9		abid	|- ( x e. { x | E! y x F y } <-> E! y x F y )
10		tz6.12-1	|- ( ( x F y /\ E! y x F y ) -> ( F ` x ) = y )
11	10	ancoms	|- ( ( E! y x F y /\ x F y ) -> ( F ` x ) = y )
12	9 11	sylanb	|- ( ( x e. { x | E! y x F y } /\ x F y ) -> ( F ` x ) = y )
13	12	eqcomd	|- ( ( x e. { x | E! y x F y } /\ x F y ) -> y = ( F ` x ) )
14	8 13	sylbi	|- ( x ( F |` { x | E! y x F y } ) y -> y = ( F ` x ) )
15	6 14	mpg	|- E. z A. y ( x ( F |` { x | E! y x F y } ) y -> y = z )
16	15	ax-gen	|- A. x E. z A. y ( x ( F |` { x | E! y x F y } ) y -> y = z )
17		nfcv	|- F/_ x F
18		nfab1	|- F/_ x { x | E! y x F y }
19	17 18	nfres	|- F/_ x ( F |` { x | E! y x F y } )
20		nfcv	|- F/_ y F
21		nfeu1	|- F/ y E! y x F y
22	21	nfab	|- F/_ y { x | E! y x F y }
23	20 22	nfres	|- F/_ y ( F |` { x | E! y x F y } )
24		nfcv	|- F/_ z ( F |` { x | E! y x F y } )
25	19 23 24	dffun3f	|- ( Fun ( F |` { x | E! y x F y } ) <-> ( Rel ( F |` { x | E! y x F y } ) /\ A. x E. z A. y ( x ( F |` { x | E! y x F y } ) y -> y = z ) ) )
26	1 16 25	mpbir2an	|- Fun ( F |` { x | E! y x F y } )