Metamath Proof Explorer

Theorem csbwrecsg

Description: Move class substitution in and out of the well-founded recursive function generator. (Contributed by ML, 25-Oct-2020)

Ref Expression
Assertion csbwrecsg 
|- ( A e. V -> [_ A / x ]_ wrecs ( R , D , F ) = wrecs ( [_ 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 ) = ( 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 ) = ( 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 ) = ( 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 ) = ( 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 ) = ( 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 ) = ( 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 ) = ( 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 ) = ( 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 8 sseq2d 
 |-  ( A e. V -> ( [_ A / x ]_ Pred ( R , D , y ) C_ [_ A / x ]_ z <-> [_ A / x ]_ Pred ( R , D , y ) C_ z ) )
14 csbpredg 
 |-  ( A e. V -> [_ A / x ]_ Pred ( R , D , y ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ y ) )
15 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ y = y )
16 predeq3 
 |-  ( [_ A / x ]_ y = y -> Pred ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ y ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) )
17 15 16 syl 
 |-  ( A e. V -> Pred ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ y ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) )
18 14 17 eqtrd 
 |-  ( A e. V -> [_ A / x ]_ Pred ( R , D , y ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) )
19 18 sseq1d 
 |-  ( A e. V -> ( [_ A / x ]_ Pred ( R , D , y ) C_ z <-> Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) )
20 12 13 19 3bitrd 
 |-  ( A e. V -> ( [. A / x ]. Pred ( R , D , y ) C_ z <-> Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) C_ z ) )
21 20 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 ) )
22 11 21 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 ) )
23 10 22 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 ) ) )
24 6 23 syl5bb 
 |-  ( 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 ) ) )
25 sbcralg 
 |-  ( A e. V -> ( [. A / x ]. A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) <-> A. y e. z [. A / x ]. ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) )
26 sbceqg 
 |-  ( A e. V -> ( [. A / x ]. ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) <-> [_ A / x ]_ ( f ` y ) = [_ A / x ]_ ( F ` ( f |` Pred ( R , D , y ) ) ) ) )
27 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ ( f ` y ) = ( f ` y ) )
28 csbfv12 
 |-  [_ A / x ]_ ( F ` ( f |` Pred ( R , D , y ) ) ) = ( [_ A / x ]_ F ` [_ A / x ]_ ( f |` Pred ( R , D , y ) ) )
29 csbres 
 |-  [_ A / x ]_ ( f |` Pred ( R , D , y ) ) = ( [_ A / x ]_ f |` [_ A / x ]_ Pred ( R , D , y ) )
30 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ f = f )
31 30 18 reseq12d 
 |-  ( A e. V -> ( [_ A / x ]_ f |` [_ A / x ]_ Pred ( R , D , y ) ) = ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) )
32 29 31 syl5eq 
 |-  ( A e. V -> [_ A / x ]_ ( f |` Pred ( R , D , y ) ) = ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) )
33 32 fveq2d 
 |-  ( A e. V -> ( [_ A / x ]_ F ` [_ A / x ]_ ( f |` Pred ( R , D , y ) ) ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) )
34 28 33 syl5eq 
 |-  ( A e. V -> [_ A / x ]_ ( F ` ( f |` Pred ( R , D , y ) ) ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) )
35 27 34 eqeq12d 
 |-  ( A e. V -> ( [_ A / x ]_ ( f ` y ) = [_ A / x ]_ ( F ` ( f |` Pred ( R , D , y ) ) ) <-> ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) )
36 26 35 bitrd 
 |-  ( A e. V -> ( [. A / x ]. ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) <-> ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) )
37 36 ralbidv 
 |-  ( A e. V -> ( A. y e. z [. A / x ]. ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) <-> A. y e. z ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) )
38 25 37 bitrd 
 |-  ( A e. V -> ( [. A / x ]. A. y e. z ( f ` y ) = ( F ` ( f |` Pred ( R , D , y ) ) ) <-> A. y e. z ( f ` y ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) )
39 5 24 38 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 ) = ( 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 ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) ) )
40 4 39 syl5bb 
 |-  ( 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 ) = ( 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 ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) ) )
41 40 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 ) = ( 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 ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) ) )
42 3 41 syl5bb 
 |-  ( 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 ) = ( 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 ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) ) )
43 42 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 ) = ( 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 ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) } )
44 2 43 syl5eq 
 |-  ( 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 ) = ( 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 ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) } )
45 44 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 ) = ( 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 ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) } )
46 1 45 syl5eq 
 |-  ( 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 ) = ( 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 ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) } )
47 df-wrecs 
 |-  wrecs ( 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 ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) }
48 47 csbeq2i 
 |-  [_ A / x ]_ wrecs ( 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 ) = ( F ` ( f |` Pred ( R , D , y ) ) ) ) }
49 df-wrecs 
 |-  wrecs ( [_ 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 ) = ( [_ A / x ]_ F ` ( f |` Pred ( [_ A / x ]_ R , [_ A / x ]_ D , y ) ) ) ) }
50 46 48 49 3eqtr4g 
 |-  ( A e. V -> [_ A / x ]_ wrecs ( R , D , F ) = wrecs ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ F ) )