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 29579
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 29578 . 2 class seqstr
2 vm . . 3 setvar 𝑚
3 vf . . 3 setvar 𝑓
4 cvv 3172 . . 3 class V
52cv 1473 . . . 4 class 𝑚
6 clsw 13093 . . . . 5 class lastS
7 vx . . . . . . 7 setvar 𝑥
8 vy . . . . . . 7 setvar 𝑦
97cv 1473 . . . . . . . 8 class 𝑥
103cv 1473 . . . . . . . . . 10 class 𝑓
119, 10cfv 5790 . . . . . . . . 9 class (𝑓𝑥)
1211cs1 13095 . . . . . . . 8 class ⟨“(𝑓𝑥)”⟩
13 cconcat 13094 . . . . . . . 8 class ++
149, 12, 13co 6527 . . . . . . 7 class (𝑥 ++ ⟨“(𝑓𝑥)”⟩)
157, 8, 4, 4, 14cmpt2 6529 . . . . . 6 class (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩))
16 cn0 11139 . . . . . . 7 class 0
175, 10cfv 5790 . . . . . . . . . 10 class (𝑓𝑚)
1817cs1 13095 . . . . . . . . 9 class ⟨“(𝑓𝑚)”⟩
195, 18, 13co 6527 . . . . . . . 8 class (𝑚 ++ ⟨“(𝑓𝑚)”⟩)
2019csn 4124 . . . . . . 7 class {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}
2116, 20cxp 5026 . . . . . 6 class (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})
22 chash 12934 . . . . . . 7 class #
235, 22cfv 5790 . . . . . 6 class (#‘𝑚)
2415, 21, 23cseq 12618 . . . . 5 class seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}))
256, 24ccom 5032 . . . 4 class ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))
265, 25cun 3537 . . 3 class (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}))))
272, 3, 4, 4, 26cmpt2 6529 . 2 class (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))))
281, 27wceq 1474 1 wff seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))))
Colors of variables: wff setvar class
This definition is referenced by:  sseqval  29583
  Copyright terms: Public domain W3C validator