Metamath Proof Explorer

Theorem wfrlem3OLDa

Description: Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. Show membership in the class of acceptable functions. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 31-Jul-2020)

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