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 ⊢ G = seq ω F I
Assertion seqom0g ⊢ I ∈ V → G ⁡ ∅ = I

Proof

Step Hyp Ref Expression
1 seqom.a ⊢ G = seq ω F I
2 df-seqom ⊢ seq ω F I = rec ⁡ a ∈ ω , b ∈ V ⟼ suc ⁡ a a F b ∅ I ⁡ I ω
3 1 2 eqtri ⊢ G = rec ⁡ a ∈ ω , b ∈ V ⟼ suc ⁡ a a F b ∅ I ⁡ I ω
4 3 fveq1i ⊢ G ⁡ ∅ = rec ⁡ a ∈ ω , b ∈ V ⟼ suc ⁡ a a F b ∅ I ⁡ I ω ⁡ ∅
5 seqomlem0 ⊢ rec ⁡ a ∈ ω , b ∈ V ⟼ suc ⁡ a a F b ∅ I ⁡ I = rec ⁡ c ∈ ω , d ∈ V ⟼ suc ⁡ c c F d ∅ I ⁡ I
6 5 seqomlem3 ⊢ rec ⁡ a ∈ ω , b ∈ V ⟼ suc ⁡ a a F b ∅ I ⁡ I ω ⁡ ∅ = I ⁡ I
7 4 6 eqtri ⊢ G ⁡ ∅ = I ⁡ I
8 fvi ⊢ I ∈ V → I ⁡ I = I
9 7 8 eqtrid ⊢ I ∈ V → G ⁡ ∅ = I