This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )