Metamath Proof Explorer

Theorem dfwrecsOLD

Description: Obsolete definition of the well-ordered recursive function generator as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 7-Jun-2018)

Ref Expression
Assertion dfwrecsOLD 
|- wrecs ( R , A , F ) = 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 ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }

Proof

Step Hyp Ref Expression
1 df-wrecs 
 |-  wrecs ( R , A , F ) = frecs ( R , A , ( F o. 2nd ) )
2 df-frecs 
 |-  frecs ( R , A , ( F o. 2nd ) ) = 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 ( F o. 2nd ) ( f |` Pred ( R , A , y ) ) ) ) }
3 vex 
 |-  y e. _V
4 3 a1i 
 |-  ( T. -> y e. _V )
5 vex 
 |-  f e. _V
6 5 resex 
 |-  ( f |` Pred ( R , A , y ) ) e. _V
7 6 a1i 
 |-  ( T. -> ( f |` Pred ( R , A , y ) ) e. _V )
8 4 7 opco2 
 |-  ( T. -> ( y ( F o. 2nd ) ( f |` Pred ( R , A , y ) ) ) = ( F ` ( f |` Pred ( R , A , y ) ) ) )
9 8 mptru 
 |-  ( y ( F o. 2nd ) ( f |` Pred ( R , A , y ) ) ) = ( F ` ( f |` Pred ( R , A , y ) ) )
10 9 eqeq2i 
 |-  ( ( f ` y ) = ( y ( F o. 2nd ) ( f |` Pred ( R , A , y ) ) ) <-> ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) )
11 10 ralbii 
 |-  ( A. y e. x ( f ` y ) = ( y ( F o. 2nd ) ( f |` Pred ( R , A , y ) ) ) <-> A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) )
12 11 3anbi3i 
 |-  ( ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y ( F o. 2nd ) ( f |` Pred ( R , A , y ) ) ) ) <-> ( 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 ) ) ) ) )
13 12 exbii 
 |-  ( 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 ( F o. 2nd ) ( f |` Pred ( R , A , y ) ) ) ) <-> 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 ) ) ) ) )
14 13 abbii 
 |-  { 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 ( F o. 2nd ) ( f |` Pred ( R , A , y ) ) ) ) } = { 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 ) ) ) ) }
15 14 unieqi 
 |-  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 ( F o. 2nd ) ( f |` Pred ( R , A , y ) ) ) ) } = 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 ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }
16 1 2 15 3eqtri 
 |-  wrecs ( R , A , F ) = 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 ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }