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=seqωFI
Assertion seqom0g IVG=I

Proof

Step Hyp Ref Expression
1 seqom.a G=seqωFI
2 df-seqom seqωFI=recaω,bVsucaaFbIIω
3 1 2 eqtri G=recaω,bVsucaaFbIIω
4 3 fveq1i G=recaω,bVsucaaFbIIω
5 seqomlem0 recaω,bVsucaaFbII=reccω,dVsucccFdII
6 5 seqomlem3 recaω,bVsucaaFbIIω=II
7 4 6 eqtri G=II
8 fvi IVII=I
9 7 8 eqtrid IVG=I