Definition df-sseq 30446

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 ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) ) ) ) )

Distinct variable group:   f, m, x, y

Detailed syntax breakdown of Definition df-sseq

Step	Hyp	Ref	Expression
1		csseq 30445	. 2 class seqstr
2		vm	. . 3 setvar m
3		vf	. . 3 setvar f
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . 4 class m
6		clsw 13292	. . . . 5 class lastS
7		vx	. . . . . . 7 setvar x
8		vy	. . . . . . 7 setvar y
9	7	cv 1482	. . . . . . . 8 class x
10	3	cv 1482	. . . . . . . . . 10 class f
11	9, 10	cfv 5888	. . . . . . . . 9 class ( f ` x )
12	11	cs1 13294	. . . . . . . 8 class <" ( f ` x ) ">
13		cconcat 13293	. . . . . . . 8 class ++
14	9, 12, 13	co 6650	. . . . . . 7 class ( x ++ <" ( f ` x ) "> )
15	7, 8, 4, 4, 14	cmpt2 6652	. . . . . 6 class ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) )
16		cn0 11292	. . . . . . 7 class NN0
17	5, 10	cfv 5888	. . . . . . . . . 10 class ( f ` m )
18	17	cs1 13294	. . . . . . . . 9 class <" ( f ` m ) ">
19	5, 18, 13	co 6650	. . . . . . . 8 class ( m ++ <" ( f ` m ) "> )
20	19	csn 4177	. . . . . . 7 class { ( m ++ <" ( f ` m ) "> ) }
21	16, 20	cxp 5112	. . . . . 6 class ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } )
22		chash 13117	. . . . . . 7 class #
23	5, 22	cfv 5888	. . . . . 6 class ( # ` m )
24	15, 21, 23	cseq 12801	. . . . 5 class seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) )
25	6, 24	ccom 5118	. . . 4 class ( lastS o. seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) ) )
26	5, 25	cun 3572	. . 3 class ( m u. ( lastS o. seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) ) ) )
27	2, 3, 4, 4, 26	cmpt2 6652	. 2 class ( 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 ) "> ) } ) ) ) ) )
28	1, 27	wceq 1483	1 wff 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 ) "> ) } ) ) ) ) )

This definition is referenced by:  sseqval  30450