Metamath Proof Explorer

Theorem rdgsucg

Description: The value of the recursive definition generator at a successor. (Contributed by NM, 16-Nov-2014)

Ref Expression
Assertion rdgsucg ⊢B∈dom⁡rec⁡FA→rec⁡FA⁡suc⁡B=F⁡rec⁡FA⁡B

Proof

Step Hyp Ref Expression
1 rdgdmlim ⊢Lim⁡dom⁡rec⁡FA
2 limsuc ⊢Lim⁡dom⁡rec⁡FA→B∈dom⁡rec⁡FA↔suc⁡B∈dom⁡rec⁡FA
3 1 2 ax-mp ⊢B∈dom⁡rec⁡FA↔suc⁡B∈dom⁡rec⁡FA
4 eqid ⊢x∈V⟼ifx=∅AifLim⁡dom⁡x⋃ran⁡xF⁡x⁡⋃dom⁡x=x∈V⟼ifx=∅AifLim⁡dom⁡x⋃ran⁡xF⁡x⁡⋃dom⁡x
5 rdgvalg ⊢y∈dom⁡rec⁡FA→rec⁡FA⁡y=x∈V⟼ifx=∅AifLim⁡dom⁡x⋃ran⁡xF⁡x⁡⋃dom⁡x⁡rec⁡FA↾y
6 rdgseg ⊢y∈dom⁡rec⁡FA→rec⁡FA↾y∈V
7 rdgfun ⊢Fun⁡rec⁡FA
8 funfn ⊢Fun⁡rec⁡FA↔rec⁡FAFndom⁡rec⁡FA
9 7 8 mpbi ⊢rec⁡FAFndom⁡rec⁡FA
10 limord ⊢Lim⁡dom⁡rec⁡FA→Ord⁡dom⁡rec⁡FA
11 1 10 ax-mp ⊢Ord⁡dom⁡rec⁡FA
12 4 5 6 9 11 tz7.44-2 ⊢suc⁡B∈dom⁡rec⁡FA→rec⁡FA⁡suc⁡B=F⁡rec⁡FA⁡B
13 3 12 sylbi ⊢B∈dom⁡rec⁡FA→rec⁡FA⁡suc⁡B=F⁡rec⁡FA⁡B