Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sseq Structured version   Visualization version   GIF version

Definition df-sseq 31541
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
StepHypRef Expression
1 csseq 31540 . 2 class seqstr
2 vm . . 3 setvar 𝑚
3 vf . . 3 setvar 𝑓
4 cvv 3492 . . 3 class V
52cv 1527 . . . 4 class 𝑚
6 clsw 13902 . . . . 5 class lastS
7 vx . . . . . . 7 setvar 𝑥
8 vy . . . . . . 7 setvar 𝑦
97cv 1527 . . . . . . . 8 class 𝑥
103cv 1527 . . . . . . . . . 10 class 𝑓
119, 10cfv 6348 . . . . . . . . 9 class (𝑓𝑥)
1211cs1 13937 . . . . . . . 8 class ⟨“(𝑓𝑥)”⟩
13 cconcat 13910 . . . . . . . 8 class ++
149, 12, 13co 7145 . . . . . . 7 class (𝑥 ++ ⟨“(𝑓𝑥)”⟩)
157, 8, 4, 4, 14cmpo 7147 . . . . . 6 class (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩))
16 cn0 11885 . . . . . . 7 class 0
175, 10cfv 6348 . . . . . . . . . 10 class (𝑓𝑚)
1817cs1 13937 . . . . . . . . 9 class ⟨“(𝑓𝑚)”⟩
195, 18, 13co 7145 . . . . . . . 8 class (𝑚 ++ ⟨“(𝑓𝑚)”⟩)
2019csn 4557 . . . . . . 7 class {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}
2116, 20cxp 5546 . . . . . 6 class (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})
22 chash 13678 . . . . . . 7 class
235, 22cfv 6348 . . . . . 6 class (♯‘𝑚)
2415, 21, 23cseq 13357 . . . . 5 class seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}))
256, 24ccom 5552 . . . 4 class (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))
265, 25cun 3931 . . 3 class (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}))))
272, 3, 4, 4, 26cmpo 7147 . 2 class (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))))
281, 27wceq 1528 1 wff seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))))
Colors of variables: wff setvar class
This definition is referenced by:  sseqval  31545
  Copyright terms: Public domain W3C validator