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
|
syl5eq |
|- ( 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
|
syl5eq |
|- ( 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
|
syl5eq |
|- ( 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 ) ) |