This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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