Definition df-seqom

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

	Ref	Expression
Assertion	df-seqom	⊢ seqω ( 𝐹 , 𝐼 ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) “ ω )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	⊢ 𝐹
1		cI	⊢ 𝐼
2	0 1	cseqom	⊢ seqω ( 𝐹 , 𝐼 )
3		vi	⊢ 𝑖
4		com	⊢ ω
5		vv	⊢ 𝑣
6		cvv	⊢ V
7	3	cv	⊢ 𝑖
8	7	csuc	⊢ suc 𝑖
9	5	cv	⊢ 𝑣
10	7 9 0	co	⊢ ( 𝑖 𝐹 𝑣 )
11	8 10	cop	⊢ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩
12	3 5 4 6 11	cmpo	⊢ ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ )
13		c0	⊢ ∅
14		cid	⊢ I
15	1 14	cfv	⊢ ( I ‘ 𝐼 )
16	13 15	cop	⊢ ⟨ ∅ , ( I ‘ 𝐼 ) ⟩
17	12 16	crdg	⊢ rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ )
18	17 4	cima	⊢ ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) “ ω )
19	2 18	wceq	⊢ seqω ( 𝐹 , 𝐼 ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) “ ω )