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

Definition df-seqom 7115
Description: Index-aware recursive definitions over  om. A mashup of df-rdg 7078 and df-seq 12087, 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
StepHypRef Expression
1 cF . . 3  class  F
2 cI . . 3  class  I
31, 2cseqom 7114 . 2  class seq𝜔 ( F ,  I
)
4 vi . . . . 5  setvar  i
5 vv . . . . 5  setvar  v
6 com 6685 . . . . 5  class  om
7 cvv 3095 . . . . 5  class  _V
84cv 1382 . . . . . . 7  class  i
98csuc 4870 . . . . . 6  class  suc  i
105cv 1382 . . . . . . 7  class  v
118, 10, 1co 6281 . . . . . 6  class  ( i F v )
129, 11cop 4020 . . . . 5  class  <. suc  i ,  ( i F v ) >.
134, 5, 6, 7, 12cmpt2 6283 . . . 4  class  ( i  e.  om ,  v  e.  _V  |->  <. suc  i ,  ( i F v ) >. )
14 c0 3770 . . . . 5  class  (/)
15 cid 4780 . . . . . 6  class  _I
162, 15cfv 5578 . . . . 5  class  (  _I 
`  I )
1714, 16cop 4020 . . . 4  class  <. (/) ,  (  _I  `  I )
>.
1813, 17crdg 7077 . . 3  class  rec (
( i  e.  om ,  v  e.  _V  |->  <. suc  i ,  ( i F v )
>. ) ,  <. (/) ,  (  _I  `  I )
>. )
1918, 6cima 4992 . 2  class  ( rec ( ( i  e. 
om ,  v  e. 
_V  |->  <. suc  i , 
( i F v ) >. ) ,  <. (/)
,  (  _I  `  I ) >. ) " om )
203, 19wceq 1383 1  wff seq𝜔 ( F ,  I
)  =  ( rec ( ( i  e. 
om ,  v  e. 
_V  |->  <. suc  i , 
( i F v ) >. ) ,  <. (/)
,  (  _I  `  I ) >. ) " om )
Colors of variables: wff setvar class
This definition is referenced by:  seqomeq12  7121  fnseqom  7122  seqom0g  7123  seqomsuc  7124
  Copyright terms: Public domain W3C validator