Definition df-sseq 34421

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

Distinct variable group:   𝑓,𝑚,𝑥,𝑦

Detailed syntax breakdown of Definition df-sseq

Step	Hyp	Ref	Expression
1		csseq 34420	. 2 class seqstr
2		vm	. . 3 setvar 𝑚
3		vf	. . 3 setvar 𝑓
4		cvv 3464	. . 3 class V
5	2	cv 1539	. . . 4 class 𝑚
6		clsw 14585	. . . . 5 class lastS
7		vx	. . . . . . 7 setvar 𝑥
8		vy	. . . . . . 7 setvar 𝑦
9	7	cv 1539	. . . . . . . 8 class 𝑥
10	3	cv 1539	. . . . . . . . . 10 class 𝑓
11	9, 10	cfv 6536	. . . . . . . . 9 class (𝑓‘𝑥)
12	11	cs1 14618	. . . . . . . 8 class ⟨“(𝑓‘𝑥)”⟩
13		cconcat 14593	. . . . . . . 8 class ++
14	9, 12, 13	co 7410	. . . . . . 7 class (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)
15	7, 8, 4, 4, 14	cmpo 7412	. . . . . 6 class (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩))
16		cn0 12506	. . . . . . 7 class ℕ0
17	5, 10	cfv 6536	. . . . . . . . . 10 class (𝑓‘𝑚)
18	17	cs1 14618	. . . . . . . . 9 class ⟨“(𝑓‘𝑚)”⟩
19	5, 18, 13	co 7410	. . . . . . . 8 class (𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)
20	19	csn 4606	. . . . . . 7 class {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)}
21	16, 20	cxp 5657	. . . . . 6 class (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)})
22		chash 14353	. . . . . . 7 class ♯
23	5, 22	cfv 6536	. . . . . 6 class (♯‘𝑚)
24	15, 21, 23	cseq 14024	. . . . 5 class seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)}))
25	6, 24	ccom 5663	. . . 4 class (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)})))
26	5, 25	cun 3929	. . 3 class (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)}))))
27	2, 3, 4, 4, 26	cmpo 7412	. 2 class (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)})))))
28	1, 27	wceq 1540	1 wff seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)})))))

This definition is referenced by:  sseqval  34425