Metamath Proof Explorer

Theorem frrlem1

Description: Lemma for well-founded recursion. The final item we are interested in is the union of acceptable functions B . This lemma just changes bound variables for later use. (Contributed by Paul Chapman, 21-Apr-2012)

Ref Expression
Hypothesis frrlem1.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 ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) }
Assertion frrlem1 
|- 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 ) = ( w G ( g |` Pred ( R , A , w ) ) ) ) }

Proof

Step Hyp Ref Expression
1 frrlem1.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 ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) }
2 fneq1 
 |-  ( f = g -> ( f Fn x <-> g Fn x ) )
3 fveq1 
 |-  ( f = g -> ( f ` y ) = ( g ` y ) )
4 reseq1 
 |-  ( f = g -> ( f |` Pred ( R , A , y ) ) = ( g |` Pred ( R , A , y ) ) )
5 4 oveq2d 
 |-  ( f = g -> ( y G ( f |` Pred ( R , A , y ) ) ) = ( y G ( g |` Pred ( R , A , y ) ) ) )
6 3 5 eqeq12d 
 |-  ( f = g -> ( ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) <-> ( g ` y ) = ( y G ( g |` Pred ( R , A , y ) ) ) ) )
7 6 ralbidv 
 |-  ( f = g -> ( A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) <-> A. y e. x ( g ` y ) = ( y G ( g |` Pred ( R , A , y ) ) ) ) )
8 2 7 3anbi13d 
 |-  ( f = g -> ( ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) <-> ( g Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( g ` y ) = ( y G ( g |` Pred ( R , A , y ) ) ) ) ) )
9 8 exbidv 
 |-  ( f = g -> ( E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) <-> E. x ( g Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( g ` y ) = ( y G ( g |` Pred ( R , A , y ) ) ) ) ) )
10 fneq2 
 |-  ( x = z -> ( g Fn x <-> g Fn z ) )
11 sseq1 
 |-  ( x = z -> ( x C_ A <-> z C_ A ) )
12 sseq2 
 |-  ( x = z -> ( Pred ( R , A , y ) C_ x <-> Pred ( R , A , y ) C_ z ) )
13 12 raleqbi1dv 
 |-  ( x = z -> ( A. y e. x Pred ( R , A , y ) C_ x <-> A. y e. z Pred ( R , A , y ) C_ z ) )
14 predeq3 
 |-  ( y = w -> Pred ( R , A , y ) = Pred ( R , A , w ) )
15 14 sseq1d 
 |-  ( y = w -> ( Pred ( R , A , y ) C_ z <-> Pred ( R , A , w ) C_ z ) )
16 15 cbvralvw 
 |-  ( A. y e. z Pred ( R , A , y ) C_ z <-> A. w e. z Pred ( R , A , w ) C_ z )
17 13 16 bitrdi 
 |-  ( x = z -> ( A. y e. x Pred ( R , A , y ) C_ x <-> A. w e. z Pred ( R , A , w ) C_ z ) )
18 11 17 anbi12d 
 |-  ( x = z -> ( ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) <-> ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) ) )
19 raleq 
 |-  ( x = z -> ( A. y e. x ( g ` y ) = ( y G ( g |` Pred ( R , A , y ) ) ) <-> A. y e. z ( g ` y ) = ( y G ( g |` Pred ( R , A , y ) ) ) ) )
20 fveq2 
 |-  ( y = w -> ( g ` y ) = ( g ` w ) )
21 id 
 |-  ( y = w -> y = w )
22 14 reseq2d 
 |-  ( y = w -> ( g |` Pred ( R , A , y ) ) = ( g |` Pred ( R , A , w ) ) )
23 21 22 oveq12d 
 |-  ( y = w -> ( y G ( g |` Pred ( R , A , y ) ) ) = ( w G ( g |` Pred ( R , A , w ) ) ) )
24 20 23 eqeq12d 
 |-  ( y = w -> ( ( g ` y ) = ( y G ( g |` Pred ( R , A , y ) ) ) <-> ( g ` w ) = ( w G ( g |` Pred ( R , A , w ) ) ) ) )
25 24 cbvralvw 
 |-  ( A. y e. z ( g ` y ) = ( y G ( g |` Pred ( R , A , y ) ) ) <-> A. w e. z ( g ` w ) = ( w G ( g |` Pred ( R , A , w ) ) ) )
26 19 25 bitrdi 
 |-  ( x = z -> ( A. y e. x ( g ` y ) = ( y G ( g |` Pred ( R , A , y ) ) ) <-> A. w e. z ( g ` w ) = ( w G ( g |` Pred ( R , A , w ) ) ) ) )
27 10 18 26 3anbi123d 
 |-  ( x = z -> ( ( g Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( g ` y ) = ( y G ( g |` Pred ( R , A , y ) ) ) ) <-> ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( w G ( g |` Pred ( R , A , w ) ) ) ) ) )
28 27 cbvexvw 
 |-  ( E. x ( g Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( g ` y ) = ( y G ( g |` Pred ( R , A , y ) ) ) ) <-> E. z ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( w G ( g |` Pred ( R , A , w ) ) ) ) )
29 9 28 bitrdi 
 |-  ( f = g -> ( E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) <-> E. z ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( w G ( g |` Pred ( R , A , w ) ) ) ) ) )
30 29 cbvabv 
 |-  { 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 ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) } = { 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 ) = ( w G ( g |` Pred ( R , A , w ) ) ) ) }
31 1 30 eqtri 
 |-  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 ) = ( w G ( g |` Pred ( R , A , w ) ) ) ) }