Metamath Proof Explorer

Theorem csbrdgg

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

Ref Expression
Assertion csbrdgg 
|- ( A e. V -> [_ A / x ]_ rec ( F , I ) = rec ( [_ A / x ]_ F , [_ A / x ]_ I ) )

Proof

Step Hyp Ref Expression
1 csbrecsg 
 |-  ( A e. V -> [_ A / x ]_ recs ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) = recs ( [_ A / x ]_ ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) )
2 csbmpt2 
 |-  ( A e. V -> [_ A / x ]_ ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) = ( g e. _V |-> [_ A / x ]_ if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
3 csbif 
 |-  [_ A / x ]_ if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) = if ( [. A / x ]. g = (/) , [_ A / x ]_ I , [_ A / x ]_ if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) )
4 sbcg 
 |-  ( A e. V -> ( [. A / x ]. g = (/) <-> g = (/) ) )
5 csbif 
 |-  [_ A / x ]_ if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) = if ( [. A / x ]. Lim dom g , [_ A / x ]_ U. ran g , [_ A / x ]_ ( F ` ( g ` U. dom g ) ) )
6 sbcg 
 |-  ( A e. V -> ( [. A / x ]. Lim dom g <-> Lim dom g ) )
7 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ U. ran g = U. ran g )
8 csbfv12 
 |-  [_ A / x ]_ ( F ` ( g ` U. dom g ) ) = ( [_ A / x ]_ F ` [_ A / x ]_ ( g ` U. dom g ) )
9 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ ( g ` U. dom g ) = ( g ` U. dom g ) )
10 9 fveq2d 
 |-  ( A e. V -> ( [_ A / x ]_ F ` [_ A / x ]_ ( g ` U. dom g ) ) = ( [_ A / x ]_ F ` ( g ` U. dom g ) ) )
11 8 10 eqtrid 
 |-  ( A e. V -> [_ A / x ]_ ( F ` ( g ` U. dom g ) ) = ( [_ A / x ]_ F ` ( g ` U. dom g ) ) )
12 6 7 11 ifbieq12d 
 |-  ( A e. V -> if ( [. A / x ]. Lim dom g , [_ A / x ]_ U. ran g , [_ A / x ]_ ( F ` ( g ` U. dom g ) ) ) = if ( Lim dom g , U. ran g , ( [_ A / x ]_ F ` ( g ` U. dom g ) ) ) )
13 5 12 eqtrid 
 |-  ( A e. V -> [_ A / x ]_ if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) = if ( Lim dom g , U. ran g , ( [_ A / x ]_ F ` ( g ` U. dom g ) ) ) )
14 4 13 ifbieq2d 
 |-  ( A e. V -> if ( [. A / x ]. g = (/) , [_ A / x ]_ I , [_ A / x ]_ if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) = if ( g = (/) , [_ A / x ]_ I , if ( Lim dom g , U. ran g , ( [_ A / x ]_ F ` ( g ` U. dom g ) ) ) ) )
15 3 14 eqtrid 
 |-  ( A e. V -> [_ A / x ]_ if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) = if ( g = (/) , [_ A / x ]_ I , if ( Lim dom g , U. ran g , ( [_ A / x ]_ F ` ( g ` U. dom g ) ) ) ) )
16 15 mpteq2dv 
 |-  ( A e. V -> ( g e. _V |-> [_ A / x ]_ if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) = ( g e. _V |-> if ( g = (/) , [_ A / x ]_ I , if ( Lim dom g , U. ran g , ( [_ A / x ]_ F ` ( g ` U. dom g ) ) ) ) ) )
17 2 16 eqtrd 
 |-  ( A e. V -> [_ A / x ]_ ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) = ( g e. _V |-> if ( g = (/) , [_ A / x ]_ I , if ( Lim dom g , U. ran g , ( [_ A / x ]_ F ` ( g ` U. dom g ) ) ) ) ) )
18 recseq 
 |-  ( [_ A / x ]_ ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) = ( g e. _V |-> if ( g = (/) , [_ A / x ]_ I , if ( Lim dom g , U. ran g , ( [_ A / x ]_ F ` ( g ` U. dom g ) ) ) ) ) -> recs ( [_ A / x ]_ ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) = recs ( ( g e. _V |-> if ( g = (/) , [_ A / x ]_ I , if ( Lim dom g , U. ran g , ( [_ A / x ]_ F ` ( g ` U. dom g ) ) ) ) ) ) )
19 17 18 syl 
 |-  ( A e. V -> recs ( [_ A / x ]_ ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) = recs ( ( g e. _V |-> if ( g = (/) , [_ A / x ]_ I , if ( Lim dom g , U. ran g , ( [_ A / x ]_ F ` ( g ` U. dom g ) ) ) ) ) ) )
20 1 19 eqtrd 
 |-  ( A e. V -> [_ A / x ]_ recs ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) = recs ( ( g e. _V |-> if ( g = (/) , [_ A / x ]_ I , if ( Lim dom g , U. ran g , ( [_ A / x ]_ F ` ( g ` U. dom g ) ) ) ) ) ) )
21 df-rdg 
 |-  rec ( F , I ) = recs ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
22 21 csbeq2i 
 |-  [_ A / x ]_ rec ( F , I ) = [_ A / x ]_ recs ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
23 df-rdg 
 |-  rec ( [_ A / x ]_ F , [_ A / x ]_ I ) = recs ( ( g e. _V |-> if ( g = (/) , [_ A / x ]_ I , if ( Lim dom g , U. ran g , ( [_ A / x ]_ F ` ( g ` U. dom g ) ) ) ) ) )
24 20 22 23 3eqtr4g 
 |-  ( A e. V -> [_ A / x ]_ rec ( F , I ) = rec ( [_ A / x ]_ F , [_ A / x ]_ I ) )