Metamath Proof Explorer

Theorem seqomsuc

Description: Value of an index-aware recursive definition at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Hypothesis seqom.a 
|- G = seqom ( F , I )
Assertion seqomsuc 
|- ( A e. _om -> ( G ` suc A ) = ( A F ( G ` A ) ) )

Proof

Step Hyp Ref Expression
1 seqom.a 
 |-  G = seqom ( F , I )
2 seqomlem0 
 |-  rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) = rec ( ( c e. _om , d e. _V |-> <. suc c , ( c F d ) >. ) , <. (/) , ( _I ` I ) >. )
3 2 seqomlem4 
 |-  ( A e. _om -> ( ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om ) ` suc A ) = ( A F ( ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om ) ` A ) ) )
4 df-seqom 
 |-  seqom ( F , I ) = ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om )
5 1 4 eqtri 
 |-  G = ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om )
6 5 fveq1i 
 |-  ( G ` suc A ) = ( ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om ) ` suc A )
7 5 fveq1i 
 |-  ( G ` A ) = ( ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om ) ` A )
8 7 oveq2i 
 |-  ( A F ( G ` A ) ) = ( A F ( ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om ) ` A ) )
9 3 6 8 3eqtr4g 
 |-  ( A e. _om -> ( G ` suc A ) = ( A F ( G ` A ) ) )