Metamath Proof Explorer

Theorem frsuc

Description: The successor value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion frsuc ⊢ B ∈ ω → rec ⁡ F A ↾ ω ⁡ suc ⁡ B = F ⁡ rec ⁡ F A ↾ ω ⁡ B

Proof

Step Hyp Ref Expression
1 rdgdmlim ⊢ Lim ⁡ dom ⁡ rec ⁡ F A
2 limomss ⊢ Lim ⁡ dom ⁡ rec ⁡ F A → ω ⊆ dom ⁡ rec ⁡ F A
3 1 2 ax-mp ⊢ ω ⊆ dom ⁡ rec ⁡ F A
4 3 sseli ⊢ B ∈ ω → B ∈ dom ⁡ rec ⁡ F A
5 rdgsucg ⊢ B ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ⁡ suc ⁡ B = F ⁡ rec ⁡ F A ⁡ B
6 4 5 syl ⊢ B ∈ ω → rec ⁡ F A ⁡ suc ⁡ B = F ⁡ rec ⁡ F A ⁡ B
7 peano2b ⊢ B ∈ ω ↔ suc ⁡ B ∈ ω
8 fvres ⊢ suc ⁡ B ∈ ω → rec ⁡ F A ↾ ω ⁡ suc ⁡ B = rec ⁡ F A ⁡ suc ⁡ B
9 7 8 sylbi ⊢ B ∈ ω → rec ⁡ F A ↾ ω ⁡ suc ⁡ B = rec ⁡ F A ⁡ suc ⁡ B
10 fvres ⊢ B ∈ ω → rec ⁡ F A ↾ ω ⁡ B = rec ⁡ F A ⁡ B
11 10 fveq2d ⊢ B ∈ ω → F ⁡ rec ⁡ F A ↾ ω ⁡ B = F ⁡ rec ⁡ F A ⁡ B
12 6 9 11 3eqtr4d ⊢ B ∈ ω → rec ⁡ F A ↾ ω ⁡ suc ⁡ B = F ⁡ rec ⁡ F A ↾ ω ⁡ B