Metamath Proof Explorer

Definition df-sseq

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)

Ref Expression
Assertion df-sseq 
|- seqstr = ( m e. _V , f e. _V |-> ( m u. ( lastS o. seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csseq 
 |-  seqstr
1 vm 
 |-  m
2 cvv 
 |-  _V
3 vf 
 |-  f
4 1 cv 
 |-  m
5 clsw 
 |-  lastS
6 chash 
 |-  #
7 4 6 cfv 
 |-  ( # ` m )
8 vx 
 |-  x
9 vy 
 |-  y
10 8 cv 
 |-  x
11 cconcat 
 |-  ++
12 3 cv 
 |-  f
13 10 12 cfv 
 |-  ( f ` x )
14 13 cs1 
 |-  <" ( f ` x ) ">
15 10 14 11 co 
 |-  ( x ++ <" ( f ` x ) "> )
16 8 9 2 2 15 cmpo 
 |-  ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) )
17 cn0 
 |-  NN0
18 4 12 cfv 
 |-  ( f ` m )
19 18 cs1 
 |-  <" ( f ` m ) ">
20 4 19 11 co 
 |-  ( m ++ <" ( f ` m ) "> )
21 20 csn 
 |-  { ( m ++ <" ( f ` m ) "> ) }
22 17 21 cxp 
 |-  ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } )
23 16 22 7 cseq 
 |-  seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) )
24 5 23 ccom 
 |-  ( lastS o. seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) ) )
25 4 24 cun 
 |-  ( m u. ( lastS o. seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) ) ) )
26 1 3 2 2 25 cmpo 
 |-  ( m e. _V , f e. _V |-> ( m u. ( lastS o. seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) ) ) ) )
27 0 26 wceq 
 |-  seqstr = ( m e. _V , f e. _V |-> ( m u. ( lastS o. seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) ) ) ) )