Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sseq Structured version   Unicode version

Definition df-sseq 26766
Description: Define a builder for sequences by strong recursion, i.e. by computing the value of the n-th element of the sequence from all preceding elements and not just the previous one. (Contributed by Thierry Arnoux, 21-Apr-2019.)
Assertion
Ref Expression
df-sseq  |- seqstr  =  ( m  e.  _V ,  f  e.  _V  |->  ( m  u.  ( lastS  o.  seq ( # `  m ) ( ( x  e. 
_V ,  y  e. 
_V  |->  ( x concat  <" (
f `  x ) "> ) ) ,  ( NN0  X.  {
( m concat  <" (
f `  m ) "> ) } ) ) ) ) )
Distinct variable group:    f, m, x, y

Detailed syntax breakdown of Definition df-sseq
StepHypRef Expression
1 csseq 26765 . 2  class seqstr
2 vm . . 3  setvar  m
3 vf . . 3  setvar  f
4 cvv 2971 . . 3  class  _V
52cv 1368 . . . 4  class  m
6 clsw 12221 . . . . 5  class lastS
7 vx . . . . . . 7  setvar  x
8 vy . . . . . . 7  setvar  y
97cv 1368 . . . . . . . 8  class  x
103cv 1368 . . . . . . . . . 10  class  f
119, 10cfv 5417 . . . . . . . . 9  class  ( f `
 x )
1211cs1 12223 . . . . . . . 8  class  <" (
f `  x ) ">
13 cconcat 12222 . . . . . . . 8  class concat
149, 12, 13co 6090 . . . . . . 7  class  ( x concat  <" ( f `  x ) "> )
157, 8, 4, 4, 14cmpt2 6092 . . . . . 6  class  ( x  e.  _V ,  y  e.  _V  |->  ( x concat  <" ( f `  x ) "> ) )
16 cn0 10578 . . . . . . 7  class  NN0
175, 10cfv 5417 . . . . . . . . . 10  class  ( f `
 m )
1817cs1 12223 . . . . . . . . 9  class  <" (
f `  m ) ">
195, 18, 13co 6090 . . . . . . . 8  class  ( m concat  <" ( f `  m ) "> )
2019csn 3876 . . . . . . 7  class  { ( m concat  <" ( f `
 m ) "> ) }
2116, 20cxp 4837 . . . . . 6  class  ( NN0 
X.  { ( m concat  <" ( f `  m ) "> ) } )
22 chash 12102 . . . . . . 7  class  #
235, 22cfv 5417 . . . . . 6  class  ( # `  m )
2415, 21, 23cseq 11805 . . . . 5  class  seq ( # `
 m ) ( ( x  e.  _V ,  y  e.  _V  |->  ( x concat  <" (
f `  x ) "> ) ) ,  ( NN0  X.  {
( m concat  <" (
f `  m ) "> ) } ) )
256, 24ccom 4843 . . . 4  class  ( lastS  o.  seq ( # `  m
) ( ( x  e.  _V ,  y  e.  _V  |->  ( x concat  <" ( f `  x ) "> ) ) ,  ( NN0  X.  { ( m concat  <" ( f `
 m ) "> ) } ) ) )
265, 25cun 3325 . . 3  class  ( m  u.  ( lastS  o.  seq ( # `  m ) ( ( x  e. 
_V ,  y  e. 
_V  |->  ( x concat  <" (
f `  x ) "> ) ) ,  ( NN0  X.  {
( m concat  <" (
f `  m ) "> ) } ) ) ) )
272, 3, 4, 4, 26cmpt2 6092 . 2  class  ( m  e.  _V ,  f  e.  _V  |->  ( m  u.  ( lastS  o.  seq ( # `  m ) ( ( x  e. 
_V ,  y  e. 
_V  |->  ( x concat  <" (
f `  x ) "> ) ) ,  ( NN0  X.  {
( m concat  <" (
f `  m ) "> ) } ) ) ) ) )
281, 27wceq 1369 1  wff seqstr  =  ( m  e.  _V ,  f  e.  _V  |->  ( m  u.  ( lastS  o.  seq ( # `  m ) ( ( x  e. 
_V ,  y  e. 
_V  |->  ( x concat  <" (
f `  x ) "> ) ) ,  ( NN0  X.  {
( m concat  <" (
f `  m ) "> ) } ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  sseqval  26770
  Copyright terms: Public domain W3C validator