Metamath Proof Explorer


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 ‘ 𝐼 ) ⟩ ) “ ω )