Metamath Proof Explorer


Definition df-seqom

Description: Index-aware recursive definitions over _om . A mashup of df-rdg and df-seq , this allows for recursive definitions that use an index in the recursion in cases where Infinity is not admitted. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Assertion df-seqom
|- seqom ( F , I ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) " _om )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF
 |-  F
1 cI
 |-  I
2 0 1 cseqom
 |-  seqom ( F , I )
3 vi
 |-  i
4 com
 |-  _om
5 vv
 |-  v
6 cvv
 |-  _V
7 3 cv
 |-  i
8 7 csuc
 |-  suc i
9 5 cv
 |-  v
10 7 9 0 co
 |-  ( i F v )
11 8 10 cop
 |-  <. suc i , ( i F v ) >.
12 3 5 4 6 11 cmpo
 |-  ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. )
13 c0
 |-  (/)
14 cid
 |-  _I
15 1 14 cfv
 |-  ( _I ` I )
16 13 15 cop
 |-  <. (/) , ( _I ` I ) >.
17 12 16 crdg
 |-  rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. )
18 17 4 cima
 |-  ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) " _om )
19 2 18 wceq
 |-  seqom ( F , I ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) " _om )