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 e. dom rec ( F , A ) /\ Lim B ) -> ( rec ( F , A ) ` B ) = U. ( rec ( F , A ) " B ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) ) = ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) )
2 rdgvalg 
 |-  ( y e. dom rec ( F , A ) -> ( rec ( F , A ) ` y ) = ( ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) ) ` ( rec ( F , A ) |` y ) ) )
3 rdgseg 
 |-  ( y e. dom rec ( F , A ) -> ( rec ( F , A ) |` y ) e. _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 e. dom rec ( F , A ) /\ Lim B ) -> ( rec ( F , A ) ` B ) = U. ( rec ( F , A ) " B ) )