Theorem wfrlem2OLD

Description: Lemma for well-ordered recursion. An acceptable function is a function. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011)

	Ref	Expression
Hypothesis	wfrlem1OLD.1	|- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }
Assertion	wfrlem2OLD	|- ( g e. B -> Fun g )

Proof

Step	Hyp	Ref	Expression
1		wfrlem1OLD.1	|- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }
2	1	wfrlem1OLD	|- B = { g | E. z ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( F ` ( g |` Pred ( R , A , w ) ) ) ) }
3	2	abeq2i	|- ( g e. B <-> E. z ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( F ` ( g |` Pred ( R , A , w ) ) ) ) )
4		fnfun	|- ( g Fn z -> Fun g )
5	4	3ad2ant1	|- ( ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( F ` ( g |` Pred ( R , A , w ) ) ) ) -> Fun g )
6	5	exlimiv	|- ( E. z ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( F ` ( g |` Pred ( R , A , w ) ) ) ) -> Fun g )
7	3 6	sylbi	|- ( g e. B -> Fun g )