MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-seqom Unicode version

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
StepHypRef Expression
1 cF . . 3
2 cI . . 3
31, 2cseqom 7131 . 2
4 vi . . . . 5
5 vv . . . . 5
6 com 6700 . . . . 5
7 cvv 3109 . . . . 5
84cv 1394 . . . . . . 7
98csuc 4885 . . . . . 6
105cv 1394 . . . . . . 7
118, 10, 1co 6296 . . . . . 6
129, 11cop 4035 . . . . 5
134, 5, 6, 7, 12cmpt2 6298 . . . 4
14 c0 3784 . . . . 5
15 cid 4795 . . . . . 6
162, 15cfv 5593 . . . . 5
1714, 16cop 4035 . . . 4
1813, 17crdg 7094 . . 3
1918, 6cima 5007 . 2
203, 19wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  seqomeq12  7138  fnseqom  7139  seqom0g  7140  seqomsuc  7141
  Copyright terms: Public domain W3C validator