Definition df-seqom 7132

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

Distinct variable groups:   ,,   ,I,

Detailed syntax breakdown of Definition df-seqom

Step	Hyp	Ref	Expression
1		cF	. . 3
2		cI	. . 3
3	1, 2	cseqom 7131	. 2
4		vi	. . . . 5
5		vv	. . . . 5
6		com 6700	. . . . 5
7		cvv 3109	. . . . 5
8	4	cv 1394	. . . . . . 7
9	8	csuc 4885	. . . . . 6
10	5	cv 1394	. . . . . . 7
11	8, 10, 1	co 6296	. . . . . 6
12	9, 11	cop 4035	. . . . 5
13	4, 5, 6, 7, 12	cmpt2 6298	. . . 4
14		c0 3784	. . . . 5
15		cid 4795	. . . . . 6
16	2, 15	cfv 5593	. . . . 5
17	14, 16	cop 4035	. . . 4
18	13, 17	crdg 7094	. . 3
19	18, 6	cima 5007	. 2
20	3, 19	wceq 1395	1

This definition is referenced by:  seqomeq12  7138  fnseqom  7139  seqom0g  7140  seqomsuc  7141