Metamath Proof Explorer

Theorem dfwrecs2

Description: TODO: Replace df-wrecs with this definition, and shorten theorems using wrecs with it. (Contributed by BJ, 27-Oct-2024)

Ref Expression
Assertion dfwrecs2 
|- wrecs ( R , A , F ) = frecs ( R , A , ( F o. 2nd ) )

Proof

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