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

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐺 ‘ ∅ ) = 𝐼 )