Metamath Proof Explorer

Theorem csbfrecsg

Description: Move class substitution in and out of the well-founded recursive function generator. (Contributed by Scott Fenton, 18-Nov-2024)

Ref Expression
Assertion csbfrecsg 
|- ( A e. V -> [_ A / x ]_ frecs ( R , D , F ) = frecs ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ F ) )

Proof

Step Hyp Ref Expression
1 csbuni 
 |-  [_ A / x ]_ U. { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) } = U. [_ A / x ]_ { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) }
2 csbab 
 |-  [_ A / x ]_ { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) } = { f | [. A / x ]. E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) }
3 sbcex2 
 |-  ( [. A / x ]. E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) <-> E. z [. A / x ]. ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) )
4 sbc3an 
 |-  ( [. A / x ]. ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) <-> ( [. A / x ]. f Fn z /\ [. A / x ]. ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ [. A / x ]. A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) )
5 sbcg 
 |-  ( A e. V -> ( [. A / x ]. f Fn z <-> f Fn z ) )
6 sbcan 
 |-  ( [. A / x ]. ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) <-> ( [. A / x ]. z C_ D /\ [. A / x ]. A. y e. z Pred ( R , D , y ) C_ z ) )
7 sbcssg 
 |-  ( A e. V -> ( [. A / x ]. z C_ D <-> [_ A / x ]_ z C_ [_ A / x ]_ D ) )
8 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ z = z )
9 8 sseq1d 
 |-  ( A e. V -> ( [_ A / x ]_ z C_ [_ A / x ]_ D <-> z C_ [_ A / x ]_ D ) )
10 7 9 bitrd 
 |-  ( A e. V -> ( [. A / x ]. z C_ D <-> z C_ [_ A / x ]_ D ) )
11 sbcralg 
 |-  ( A e. V -> ( [. A / x ]. A. y e. z Pred ( R , D , y ) C_ z <-> A. y e. z [. A / x ]. Pred ( R , D , y ) C_ z ) )
12 sbcssg 
 |-  ( A e. V -> ( [. A / x ]. Pred ( R , D , y ) C_ z <-> [_ A / x ]_ Pred ( R , D , y ) C_ [_ A / x ]_ z ) )
13 csbpredg 
 |-  ( A e. V -> [_ A / x ]_ Pred ( R , D , y ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ y ) )
14 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ y = y )
15 predeq3 
 |-  ( [_ A / x ]_ y = y -> Pred ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ y ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) )
16 14 15 syl 
 |-  ( A e. V -> Pred ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ y ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) )
17 13 16 eqtrd 
 |-  ( A e. V -> [_ A / x ]_ Pred ( R , D , y ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) )
18 17 8 sseq12d 
 |-  ( A e. V -> ( [_ A / x ]_ Pred ( R , D , y ) C_ [_ A / x ]_ z <-> Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) )
19 12 18 bitrd 
 |-  ( A e. V -> ( [. A / x ]. Pred ( R , D , y ) C_ z <-> Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) )
20 19 ralbidv 
 |-  ( A e. V -> ( A. y e. z [. A / x ]. Pred ( R , D , y ) C_ z <-> A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) )
21 11 20 bitrd 
 |-  ( A e. V -> ( [. A / x ]. A. y e. z Pred ( R , D , y ) C_ z <-> A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) )
22 10 21 anbi12d 
 |-  ( A e. V -> ( ( [. A / x ]. z C_ D /\ [. A / x ]. A. y e. z Pred ( R , D , y ) C_ z ) <-> ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) ) )
23 6 22 bitrid 
 |-  ( A e. V -> ( [. A / x ]. ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) <-> ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) ) )
24 sbcralg 
 |-  ( A e. V -> ( [. A / x ]. A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) <-> A. y e. z [. A / x ]. ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) )
25 sbceqg 
 |-  ( A e. V -> ( [. A / x ]. ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) <-> [_ A / x ]_ ( f ` y ) = [_ A / x ]_ ( y F ( f |` Pred ( R , D , y ) ) ) ) )
26 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ ( f ` y ) = ( f ` y ) )
27 csbov123 
 |-  [_ A / x ]_ ( y F ( f |` Pred ( R , D , y ) ) ) = ( [_ A / x ]_ y [_ A / x ]_ F [_ A / x ]_ ( f |` Pred ( R , D , y ) ) )
28 csbres 
 |-  [_ A / x ]_ ( f |` Pred ( R , D , y ) ) = ( [_ A / x ]_ f |` [_ A / x ]_ Pred ( R , D , y ) )
29 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ f = f )
30 29 17 reseq12d 
 |-  ( A e. V -> ( [_ A / x ]_ f |` [_ A / x ]_ Pred ( R , D , y ) ) = ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) )
31 28 30 eqtrid 
 |-  ( A e. V -> [_ A / x ]_ ( f |` Pred ( R , D , y ) ) = ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) )
32 14 31 oveq12d 
 |-  ( A e. V -> ( [_ A / x ]_ y [_ A / x ]_ F [_ A / x ]_ ( f |` Pred ( R , D , y ) ) ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) )
33 27 32 eqtrid 
 |-  ( A e. V -> [_ A / x ]_ ( y F ( f |` Pred ( R , D , y ) ) ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) )
34 26 33 eqeq12d 
 |-  ( A e. V -> ( [_ A / x ]_ ( f ` y ) = [_ A / x ]_ ( y F ( f |` Pred ( R , D , y ) ) ) <-> ( f ` y ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) )
35 25 34 bitrd 
 |-  ( A e. V -> ( [. A / x ]. ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) <-> ( f ` y ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) )
36 35 ralbidv 
 |-  ( A e. V -> ( A. y e. z [. A / x ]. ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) <-> A. y e. z ( f ` y ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) )
37 24 36 bitrd 
 |-  ( A e. V -> ( [. A / x ]. A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) <-> A. y e. z ( f ` y ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) )
38 5 23 37 3anbi123d 
 |-  ( A e. V -> ( ( [. A / x ]. f Fn z /\ [. A / x ]. ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ [. A / x ]. A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) <-> ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) ) )
39 4 38 bitrid 
 |-  ( A e. V -> ( [. A / x ]. ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) <-> ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) ) )
40 39 exbidv 
 |-  ( A e. V -> ( E. z [. A / x ]. ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) <-> E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) ) )
41 3 40 bitrid 
 |-  ( A e. V -> ( [. A / x ]. E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) <-> E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) ) )
42 41 abbidv 
 |-  ( A e. V -> { f | [. A / x ]. E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) } = { f | E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) } )
43 2 42 eqtrid 
 |-  ( A e. V -> [_ A / x ]_ { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) } = { f | E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) } )
44 43 unieqd 
 |-  ( A e. V -> U. [_ A / x ]_ { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) } = U. { f | E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) } )
45 1 44 eqtrid 
 |-  ( A e. V -> [_ A / x ]_ U. { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) } = U. { f | E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) } )
46 df-frecs 
 |-  frecs ( R , D , F ) = U. { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) }
47 46 csbeq2i 
 |-  [_ A / x ]_ frecs ( R , D , F ) = [_ A / x ]_ U. { f | E. z ( f Fn z /\ ( z C_ D /\ A. y e. z Pred ( R , D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y F ( f |` Pred ( R , D , y ) ) ) ) }
48 df-frecs 
 |-  frecs ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ F ) = U. { f | E. z ( f Fn z /\ ( z C_ [_ A / x ]_ D /\ A. y e. z Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) /\ A. y e. z ( f ` y ) = ( y [_ A / x ]_ F ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) }
49 45 47 48 3eqtr4g 
 |-  ( A e. V -> [_ A / x ]_ frecs ( R , D , F ) = frecs ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ F ) )