Metamath Proof Explorer

Theorem wfrlem1

Description: Lemma for well-ordered 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 Scott Fenton, 21-Apr-2011)

Ref Expression
Hypothesis 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 ) ) ) ) }
Assertion 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 ) ) ) ) }

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 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 fveq2d 
 |-  ( f = g -> ( F ` ( f |` Pred ( R , A , y ) ) ) = ( F ` ( g |` Pred ( R , A , y ) ) ) )
6 3 5 eqeq12d 
 |-  ( f = g -> ( ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) <-> ( g ` y ) = ( F ` ( g |` Pred ( R , A , y ) ) ) ) )
7 6 ralbidv 
 |-  ( f = g -> ( A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) <-> A. y e. x ( g ` y ) = ( F ` ( 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 ) = ( F ` ( 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 ) = ( F ` ( 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 ) = ( F ` ( 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 ) = ( F ` ( 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 ) = ( F ` ( g |` Pred ( R , A , y ) ) ) <-> A. y e. z ( g ` y ) = ( F ` ( g |` Pred ( R , A , y ) ) ) ) )
20 fveq2 
 |-  ( y = w -> ( g ` y ) = ( g ` w ) )
21 14 reseq2d 
 |-  ( y = w -> ( g |` Pred ( R , A , y ) ) = ( g |` Pred ( R , A , w ) ) )
22 21 fveq2d 
 |-  ( y = w -> ( F ` ( g |` Pred ( R , A , y ) ) ) = ( F ` ( g |` Pred ( R , A , w ) ) ) )
23 20 22 eqeq12d 
 |-  ( y = w -> ( ( g ` y ) = ( F ` ( g |` Pred ( R , A , y ) ) ) <-> ( g ` w ) = ( F ` ( g |` Pred ( R , A , w ) ) ) ) )
24 23 cbvralvw 
 |-  ( A. y e. z ( g ` y ) = ( F ` ( g |` Pred ( R , A , y ) ) ) <-> A. w e. z ( g ` w ) = ( F ` ( g |` Pred ( R , A , w ) ) ) )
25 19 24 bitrdi 
 |-  ( x = z -> ( A. y e. x ( g ` y ) = ( F ` ( g |` Pred ( R , A , y ) ) ) <-> A. w e. z ( g ` w ) = ( F ` ( g |` Pred ( R , A , w ) ) ) ) )
26 10 18 25 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 ) = ( F ` ( 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 ) = ( F ` ( g |` Pred ( R , A , w ) ) ) ) ) )
27 26 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 ) = ( F ` ( 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 ) = ( F ` ( g |` Pred ( R , A , w ) ) ) ) )
28 9 27 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 ) = ( F ` ( 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 ) = ( F ` ( g |` Pred ( R , A , w ) ) ) ) ) )
29 28 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 ) = ( F ` ( 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 ) = ( F ` ( g |` Pred ( R , A , w ) ) ) ) }
30 1 29 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 ) = ( F ` ( g |` Pred ( R , A , w ) ) ) ) }