Description: Lemma for well-founded recursion. State the well-founded recursion generator in terms of the acceptable functions. (Contributed by Scott Fenton, 27-Aug-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frrlem5.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 ) ) ) ) } |
|
frrlem5.2 | |- F = frecs ( R , A , G ) |
||
Assertion | frrlem5 | |- F = U. B |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frrlem5.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 | frrlem5.2 | |- F = frecs ( R , A , G ) |
|
3 | df-frecs | |- frecs ( R , A , G ) = U. { 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 ) ) ) ) } |
|
4 | 1 | unieqi | |- U. B = U. { 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 ) ) ) ) } |
5 | 3 2 4 | 3eqtr4i | |- F = U. B |