Theorem seqom0g

Description: Value of an index-aware recursive definition at 0. (Contributed by Stefan O'Rear, 1-Nov-2014) (Revised by AV, 17-Sep-2021)

	Ref	Expression
Hypothesis	seqom.a	⊢ 𝐺 = seqω ( 𝐹 , 𝐼 )
Assertion	seqom0g	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐺 ‘ ∅ ) = 𝐼 )

Proof

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