Definition df-sseq 29773

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 29772	. 2 class seqstr
2		vm	. . 3 setvar 𝑚
3		vf	. . 3 setvar 𝑓
4		cvv 3173	. . 3 class V
5	2	cv 1474	. . . 4 class 𝑚
6		clsw 13147	. . . . 5 class lastS
7		vx	. . . . . . 7 setvar 𝑥
8		vy	. . . . . . 7 setvar 𝑦
9	7	cv 1474	. . . . . . . 8 class 𝑥
10	3	cv 1474	. . . . . . . . . 10 class 𝑓
11	9, 10	cfv 5804	. . . . . . . . 9 class (𝑓‘𝑥)
12	11	cs1 13149	. . . . . . . 8 class ⟨“(𝑓‘𝑥)”⟩
13		cconcat 13148	. . . . . . . 8 class ++
14	9, 12, 13	co 6549	. . . . . . 7 class (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)
15	7, 8, 4, 4, 14	cmpt2 6551	. . . . . 6 class (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩))
16		cn0 11169	. . . . . . 7 class ℕ0
17	5, 10	cfv 5804	. . . . . . . . . 10 class (𝑓‘𝑚)
18	17	cs1 13149	. . . . . . . . 9 class ⟨“(𝑓‘𝑚)”⟩
19	5, 18, 13	co 6549	. . . . . . . 8 class (𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)
20	19	csn 4125	. . . . . . 7 class {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)}
21	16, 20	cxp 5036	. . . . . 6 class (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)})
22		chash 12979	. . . . . . 7 class #
23	5, 22	cfv 5804	. . . . . 6 class (#‘𝑚)
24	15, 21, 23	cseq 12663	. . . . 5 class seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)}))
25	6, 24	ccom 5042	. . . 4 class ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)})))
26	5, 25	cun 3538	. . 3 class (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)}))))
27	2, 3, 4, 4, 26	cmpt2 6551	. 2 class (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)})))))
28	1, 27	wceq 1475	1 wff seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)})))))

This definition is referenced by:  sseqval  29777