wfrlem3a

Description: Lemma for well-ordered 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 ) ) ) ) )

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 ) ) ) ) )

Metamath Proof Explorer

Theorem wfrlem3a

Proof