Definition df-seqom 7543

Description: Index-aware recursive definitions over ω. A mashup of df-rdg 7506 and df-seq 12802, 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

Step	Hyp	Ref	Expression
1		cF	. . 3 class 𝐹
2		cI	. . 3 class 𝐼
3	1, 2	cseqom 7542	. 2 class seq𝜔(𝐹, 𝐼)
4		vi	. . . . 5 setvar 𝑖
5		vv	. . . . 5 setvar 𝑣
6		com 7065	. . . . 5 class ω
7		cvv 3200	. . . . 5 class V
8	4	cv 1482	. . . . . . 7 class 𝑖
9	8	csuc 5725	. . . . . 6 class suc 𝑖
10	5	cv 1482	. . . . . . 7 class 𝑣
11	8, 10, 1	co 6650	. . . . . 6 class (𝑖𝐹𝑣)
12	9, 11	cop 4183	. . . . 5 class ⟨suc 𝑖, (𝑖𝐹𝑣)⟩
13	4, 5, 6, 7, 12	cmpt2 6652	. . . 4 class (𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)
14		c0 3915	. . . . 5 class ∅
15		cid 5023	. . . . . 6 class I
16	2, 15	cfv 5888	. . . . 5 class ( I ‘𝐼)
17	14, 16	cop 4183	. . . 4 class ⟨∅, ( I ‘𝐼)⟩
18	13, 17	crdg 7505	. . 3 class rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)
19	18, 6	cima 5117	. 2 class (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) “ ω)
20	3, 19	wceq 1483	1 wff seq𝜔(𝐹, 𝐼) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) “ ω)

This definition is referenced by:  seqomeq12  7549  fnseqom  7550  seqom0g  7551  seqomsuc  7552