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 ⊢ G = seq ω F I
Assertion seqomsuc ⊢ A ∈ ω → G ⁡ suc ⁡ A = A F G ⁡ A

Proof

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