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 = ( 𝑚 ∈ V , 𝑓 ∈ V ↦ ( 𝑚 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑚 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csseq	⊢ seqstr
1		vm	⊢ 𝑚
2		cvv	⊢ V
3		vf	⊢ 𝑓
4	1	cv	⊢ 𝑚
5		clsw	⊢ lastS
6		chash	⊢ ♯
7	4 6	cfv	⊢ ( ♯ ‘ 𝑚 )
8		vx	⊢ 𝑥
9		vy	⊢ 𝑦
10	8	cv	⊢ 𝑥
11		cconcat	⊢ ++
12	3	cv	⊢ 𝑓
13	10 12	cfv	⊢ ( 𝑓 ‘ 𝑥 )
14	13	cs1	⊢ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩
15	10 14 11	co	⊢ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ )
16	8 9 2 2 15	cmpo	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) )
17		cn0	⊢ ℕ0
18	4 12	cfv	⊢ ( 𝑓 ‘ 𝑚 )
19	18	cs1	⊢ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩
20	4 19 11	co	⊢ ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ )
21	20	csn	⊢ { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) }
22	17 21	cxp	⊢ ( ℕ0 × { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } )
23	16 22 7	cseq	⊢ seq ( ♯ ‘ 𝑚 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } ) )
24	5 23	ccom	⊢ ( lastS ∘ seq ( ♯ ‘ 𝑚 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } ) ) )
25	4 24	cun	⊢ ( 𝑚 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑚 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } ) ) ) )
26	1 3 2 2 25	cmpo	⊢ ( 𝑚 ∈ V , 𝑓 ∈ V ↦ ( 𝑚 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑚 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } ) ) ) ) )
27	0 26	wceq	⊢ seqstr = ( 𝑚 ∈ V , 𝑓 ∈ V ↦ ( 𝑚 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑚 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } ) ) ) ) )