Definition df-seqom 7543

Description: Index-aware recursive definitions over om. A mashup of df-rdg 7506 and df-seq 12802, 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.)

Assertion

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

Distinct variable groups:   i, F, v   i, I, v

Detailed syntax breakdown of Definition df-seqom

Step	Hyp	Ref	Expression
1		cF	. . 3 class F
2		cI	. . 3 class I
3	1, 2	cseqom 7542	. 2 class seq𝜔 ( F , I )
4		vi	. . . . 5 setvar i
5		vv	. . . . 5 setvar v
6		com 7065	. . . . 5 class om
7		cvv 3200	. . . . 5 class _V
8	4	cv 1482	. . . . . . 7 class i
9	8	csuc 5725	. . . . . 6 class suc i
10	5	cv 1482	. . . . . . 7 class v
11	8, 10, 1	co 6650	. . . . . 6 class ( i F v )
12	9, 11	cop 4183	. . . . 5 class <. suc i , ( i F v ) >.
13	4, 5, 6, 7, 12	cmpt2 6652	. . . 4 class ( i e. om , v e. _V |-> <. suc i , ( i F v ) >. )
14		c0 3915	. . . . 5 class (/)
15		cid 5023	. . . . . 6 class _I
16	2, 15	cfv 5888	. . . . 5 class ( _I ` I )
17	14, 16	cop 4183	. . . 4 class <. (/) , ( _I ` I ) >.
18	13, 17	crdg 7505	. . 3 class rec ( ( i e. om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. )
19	18, 6	cima 5117	. 2 class ( rec ( ( i e. om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) " om )
20	3, 19	wceq 1483	1 wff seq𝜔 ( F , I ) = ( rec ( ( i e. om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) " om )

This definition is referenced by:  seqomeq12  7549  fnseqom  7550  seqom0g  7551  seqomsuc  7552