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

Metamath Proof Explorer

Theorem seqomsuc

Description: Value of an index-aware recursive definition at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Hypothesis seqom.a ⊢ 𝐺 = seqω ( 𝐹 , 𝐼 )
Assertion seqomsuc ( 𝐴 ∈ ω → ( 𝐺 ‘ suc 𝐴 ) = ( 𝐴 𝐹 ( 𝐺 ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 seqom.a ⊢ 𝐺 = seqω ( 𝐹 , 𝐼 )
2 seqomlem0 ⊢ rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐹 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) = rec ( ( 𝑐 ∈ ω , 𝑑 ∈ V ↦ ⟨ suc 𝑐 , ( 𝑐 𝐹 𝑑 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ )
3 2 seqomlem4 ⊢ ( 𝐴 ∈ ω → ( ( rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐹 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) “ ω ) ‘ suc 𝐴 ) = ( 𝐴 𝐹 ( ( rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐹 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) “ ω ) ‘ 𝐴 ) ) )
4 df-seqom ⊢ seqω ( 𝐹 , 𝐼 ) = ( rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐹 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) “ ω )
5 1 4 eqtri ⊢ 𝐺 = ( rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐹 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) “ ω )
6 5 fveq1i ⊢ ( 𝐺 ‘ suc 𝐴 ) = ( ( rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐹 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) “ ω ) ‘ suc 𝐴 )
7 5 fveq1i ⊢ ( 𝐺 ‘ 𝐴 ) = ( ( rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐹 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) “ ω ) ‘ 𝐴 )
8 7 oveq2i ⊢ ( 𝐴 𝐹 ( 𝐺 ‘ 𝐴 ) ) = ( 𝐴 𝐹 ( ( rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐹 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) “ ω ) ‘ 𝐴 ) )
9 3 6 8 3eqtr4g ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ suc 𝐴 ) = ( 𝐴 𝐹 ( 𝐺 ‘ 𝐴 ) ) )