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⁡FA↾ω⁡suc⁡B=F⁡rec⁡FA↾ω⁡B

Proof

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