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 29773
 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 29772 . 2 class seqstr
2 vm . . 3 setvar 𝑚
3 vf . . 3 setvar 𝑓
4 cvv 3173 . . 3 class V
52cv 1474 . . . 4 class 𝑚
6 clsw 13147 . . . . 5 class lastS
7 vx . . . . . . 7 setvar 𝑥
8 vy . . . . . . 7 setvar 𝑦
97cv 1474 . . . . . . . 8 class 𝑥
103cv 1474 . . . . . . . . . 10 class 𝑓
119, 10cfv 5804 . . . . . . . . 9 class (𝑓𝑥)
1211cs1 13149 . . . . . . . 8 class ⟨“(𝑓𝑥)”⟩
13 cconcat 13148 . . . . . . . 8 class ++
149, 12, 13co 6549 . . . . . . 7 class (𝑥 ++ ⟨“(𝑓𝑥)”⟩)
157, 8, 4, 4, 14cmpt2 6551 . . . . . 6 class (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩))
16 cn0 11169 . . . . . . 7 class 0
175, 10cfv 5804 . . . . . . . . . 10 class (𝑓𝑚)
1817cs1 13149 . . . . . . . . 9 class ⟨“(𝑓𝑚)”⟩
195, 18, 13co 6549 . . . . . . . 8 class (𝑚 ++ ⟨“(𝑓𝑚)”⟩)
2019csn 4125 . . . . . . 7 class {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}
2116, 20cxp 5036 . . . . . 6 class (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})
22 chash 12979 . . . . . . 7 class #
235, 22cfv 5804 . . . . . 6 class (#‘𝑚)
2415, 21, 23cseq 12663 . . . . 5 class seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}))
256, 24ccom 5042 . . . 4 class ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))
265, 25cun 3538 . . 3 class (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}))))
272, 3, 4, 4, 26cmpt2 6551 . 2 class (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))))
281, 27wceq 1475 1 wff seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))))
 Colors of variables: wff setvar class This definition is referenced by:  sseqval  29777
 Copyright terms: Public domain W3C validator