Metamath Proof Explorer

Theorem seqom0g

Description: Value of an index-aware recursive definition at 0. (Contributed by Stefan O'Rear, 1-Nov-2014) (Revised by AV, 17-Sep-2021)

Ref Expression
Hypothesis seqom.a 
|- G = seqom ( F , I )
Assertion seqom0g 
|- ( I e. V -> ( G ` (/) ) = I )

Proof

Step Hyp Ref Expression
1 seqom.a 
 |-  G = seqom ( F , I )
2 df-seqom 
 |-  seqom ( F , I ) = ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om )
3 1 2 eqtri 
 |-  G = ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om )
4 3 fveq1i 
 |-  ( G ` (/) ) = ( ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om ) ` (/) )
5 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 ) >. )
6 5 seqomlem3 
 |-  ( ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om ) ` (/) ) = ( _I ` I )
7 4 6 eqtri 
 |-  ( G ` (/) ) = ( _I ` I )
8 fvi 
 |-  ( I e. V -> ( _I ` I ) = I )
9 7 8 eqtrid 
 |-  ( I e. V -> ( G ` (/) ) = I )