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 30574
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 30573 . 2 class seqstr
2 vm . . 3 setvar 𝑚
3 vf . . 3 setvar 𝑓
4 cvv 3231 . . 3 class V
52cv 1522 . . . 4 class 𝑚
6 clsw 13324 . . . . 5 class lastS
7 vx . . . . . . 7 setvar 𝑥
8 vy . . . . . . 7 setvar 𝑦
97cv 1522 . . . . . . . 8 class 𝑥
103cv 1522 . . . . . . . . . 10 class 𝑓
119, 10cfv 5926 . . . . . . . . 9 class (𝑓𝑥)
1211cs1 13326 . . . . . . . 8 class ⟨“(𝑓𝑥)”⟩
13 cconcat 13325 . . . . . . . 8 class ++
149, 12, 13co 6690 . . . . . . 7 class (𝑥 ++ ⟨“(𝑓𝑥)”⟩)
157, 8, 4, 4, 14cmpt2 6692 . . . . . 6 class (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩))
16 cn0 11330 . . . . . . 7 class 0
175, 10cfv 5926 . . . . . . . . . 10 class (𝑓𝑚)
1817cs1 13326 . . . . . . . . 9 class ⟨“(𝑓𝑚)”⟩
195, 18, 13co 6690 . . . . . . . 8 class (𝑚 ++ ⟨“(𝑓𝑚)”⟩)
2019csn 4210 . . . . . . 7 class {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}
2116, 20cxp 5141 . . . . . 6 class (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})
22 chash 13157 . . . . . . 7 class #
235, 22cfv 5926 . . . . . 6 class (#‘𝑚)
2415, 21, 23cseq 12841 . . . . 5 class seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}))
256, 24ccom 5147 . . . 4 class ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))
265, 25cun 3605 . . 3 class (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}))))
272, 3, 4, 4, 26cmpt2 6692 . 2 class (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))))
281, 27wceq 1523 1 wff seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))))
Colors of variables: wff setvar class
This definition is referenced by:  sseqval  30578
  Copyright terms: Public domain W3C validator