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

Detailed syntax breakdown

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