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 ⊢ seq str = m ∈ V , f ∈ V ⟼ m ∪ lastS ∘ seq m x ∈ V , y ∈ V ⟼ x ++ ⟨“ f ⁡ x ”⟩ ℕ 0 × m ++ ⟨“ f ⁡ m ”⟩

Detailed syntax breakdown

Step Hyp Ref Expression
0 csseq class seq str
1 vm setvar m
2 cvv class V
3 vf setvar f
4 1 cv setvar m
5 clsw class lastS
6 chash class .
7 4 6 cfv class m
8 vx setvar x
9 vy setvar y
10 8 cv setvar x
11 cconcat class ++
12 3 cv setvar f
13 10 12 cfv class f ⁡ x
14 13 cs1 class ⟨“ f ⁡ x ”⟩
15 10 14 11 co class x ++ ⟨“ f ⁡ x ”⟩
16 8 9 2 2 15 cmpo class x ∈ V , y ∈ V ⟼ x ++ ⟨“ f ⁡ x ”⟩
17 cn0 class ℕ 0
18 4 12 cfv class f ⁡ m
19 18 cs1 class ⟨“ f ⁡ m ”⟩
20 4 19 11 co class m ++ ⟨“ f ⁡ m ”⟩
21 20 csn class m ++ ⟨“ f ⁡ m ”⟩
22 17 21 cxp class ℕ 0 × m ++ ⟨“ f ⁡ m ”⟩
23 16 22 7 cseq class seq m x ∈ V , y ∈ V ⟼ x ++ ⟨“ f ⁡ x ”⟩ ℕ 0 × m ++ ⟨“ f ⁡ m ”⟩
24 5 23 ccom class lastS ∘ seq m x ∈ V , y ∈ V ⟼ x ++ ⟨“ f ⁡ x ”⟩ ℕ 0 × m ++ ⟨“ f ⁡ m ”⟩
25 4 24 cun class m ∪ lastS ∘ seq m x ∈ V , y ∈ V ⟼ x ++ ⟨“ f ⁡ x ”⟩ ℕ 0 × m ++ ⟨“ f ⁡ m ”⟩
26 1 3 2 2 25 cmpo class m ∈ V , f ∈ V ⟼ m ∪ lastS ∘ seq m x ∈ V , y ∈ V ⟼ x ++ ⟨“ f ⁡ x ”⟩ ℕ 0 × m ++ ⟨“ f ⁡ m ”⟩
27 0 26 wceq wff seq str = m ∈ V , f ∈ V ⟼ m ∪ lastS ∘ seq m x ∈ V , y ∈ V ⟼ x ++ ⟨“ f ⁡ x ”⟩ ℕ 0 × m ++ ⟨“ f ⁡ m ”⟩