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 𝐴 ) = ( 𝐴 𝐹 ( 𝐺 ‘ 𝐴 ) ) )