Theorem wfrlem3a

Description: Lemma for well-founded recursion. Show membership in the class of acceptable functions. (Contributed by Scott Fenton, 31-Jul-2020)

	Ref	Expression
Hypotheses	wfrlem1.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 ) ) ) ) }
	wfrlem3a.2	|- G e. _V
Assertion	wfrlem3a	|- ( 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 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		wfrlem1.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		wfrlem3a.2	|- G e. _V
3		fneq1	|- ( g = G -> ( g Fn z <-> G Fn z ) )
4		fveq1	|- ( g = G -> ( g ` w ) = ( G ` w ) )
5		reseq1	|- ( g = G -> ( g |` Pred ( R , A , w ) ) = ( G |` Pred ( R , A , w ) ) )
6	5	fveq2d	|- ( g = G -> ( F ` ( g |` Pred ( R , A , w ) ) ) = ( F ` ( G |` Pred ( R , A , w ) ) ) )
7	4 6	eqeq12d	|- ( g = G -> ( ( g ` w ) = ( F ` ( g |` Pred ( R , A , w ) ) ) <-> ( G ` w ) = ( F ` ( G |` Pred ( R , A , w ) ) ) ) )
8	7	ralbidv	|- ( g = G -> ( A. w e. z ( g ` w ) = ( F ` ( g |` Pred ( R , A , w ) ) ) <-> A. w e. z ( G ` w ) = ( F ` ( G |` Pred ( R , A , w ) ) ) ) )
9	3 8	3anbi13d	|- ( g = G -> ( ( 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 ) ) ) ) <-> ( 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 ) ) ) ) ) )
10	9	exbidv	|- ( g = 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 ) ) ) ) <-> 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 ) ) ) ) ) )
11	1	wfrlem1	|- 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 ) ) ) ) }
12	2 10 11	elab2	|- ( 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 ) ) ) ) )