Metamath Proof Explorer


Theorem rdglimg

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

Ref Expression
Assertion rdglimg B dom rec F A Lim B rec F A B = rec F A B

Proof

Step Hyp Ref Expression
1 eqid x V if x = A if Lim dom x ran x F x dom x = x V if x = A if Lim dom x ran x F x dom x
2 rdgvalg y dom rec F A rec F A y = x V if x = A if Lim dom x ran x F x dom x rec F A y
3 rdgseg y dom rec F A rec F A y V
4 rdgfun Fun rec F A
5 funfn Fun rec F A rec F A Fn dom rec F A
6 4 5 mpbi rec F A Fn dom rec F A
7 rdgdmlim Lim dom rec F A
8 limord Lim dom rec F A Ord dom rec F A
9 7 8 ax-mp Ord dom rec F A
10 1 2 3 6 9 tz7.44-3 B dom rec F A Lim B rec F A B = rec F A B