MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-seqom Structured version   Visualization version   GIF version

Definition df-seqom 7779
Description: Index-aware recursive definitions over ω. A mashup of df-rdg 7742 and df-seq 13025, this allows for recursive definitions that use an index in the recursion in cases where Infinity is not admitted. (Contributed by Stefan O'Rear, 1-Nov-2014.)
Assertion
Ref Expression
df-seqom seq𝜔(𝐹, 𝐼) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) “ ω)
Distinct variable groups:   𝑖,𝐹,𝑣   𝑖,𝐼,𝑣

Detailed syntax breakdown of Definition df-seqom
StepHypRef Expression
1 cF . . 3 class 𝐹
2 cI . . 3 class 𝐼
31, 2cseqom 7778 . 2 class seq𝜔(𝐹, 𝐼)
4 vi . . . . 5 setvar 𝑖
5 vv . . . . 5 setvar 𝑣
6 com 7295 . . . . 5 class ω
7 cvv 3391 . . . . 5 class V
84cv 1636 . . . . . . 7 class 𝑖
98csuc 5938 . . . . . 6 class suc 𝑖
105cv 1636 . . . . . . 7 class 𝑣
118, 10, 1co 6874 . . . . . 6 class (𝑖𝐹𝑣)
129, 11cop 4376 . . . . 5 class ⟨suc 𝑖, (𝑖𝐹𝑣)⟩
134, 5, 6, 7, 12cmpt2 6876 . . . 4 class (𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)
14 c0 4116 . . . . 5 class
15 cid 5218 . . . . . 6 class I
162, 15cfv 6101 . . . . 5 class ( I ‘𝐼)
1714, 16cop 4376 . . . 4 class ⟨∅, ( I ‘𝐼)⟩
1813, 17crdg 7741 . . 3 class rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)
1918, 6cima 5314 . 2 class (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) “ ω)
203, 19wceq 1637 1 wff seq𝜔(𝐹, 𝐼) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) “ ω)
Colors of variables: wff setvar class
This definition is referenced by:  seqomeq12  7785  fnseqom  7786  seqom0g  7787  seqomsuc  7788
  Copyright terms: Public domain W3C validator