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 ( ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eqid ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ran 𝑥 , ( 𝐹 ‘ ( 𝑥 dom 𝑥 ) ) ) ) ) = ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ran 𝑥 , ( 𝐹 ‘ ( 𝑥 dom 𝑥 ) ) ) ) )
2 rdgvalg ( 𝑦 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ran 𝑥 , ( 𝐹 ‘ ( 𝑥 dom 𝑥 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ 𝑦 ) ) )
3 rdgseg ( 𝑦 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ↾ 𝑦 ) ∈ V )
4 rdgfun Fun rec ( 𝐹 , 𝐴 )
5 funfn ( Fun rec ( 𝐹 , 𝐴 ) ↔ rec ( 𝐹 , 𝐴 ) Fn dom rec ( 𝐹 , 𝐴 ) )
6 4 5 mpbi rec ( 𝐹 , 𝐴 ) Fn dom rec ( 𝐹 , 𝐴 )
7 rdgdmlim Lim dom rec ( 𝐹 , 𝐴 )
8 limord ( Lim dom rec ( 𝐹 , 𝐴 ) → Ord dom rec ( 𝐹 , 𝐴 ) )
9 7 8 ax-mp Ord dom rec ( 𝐹 , 𝐴 )
10 1 2 3 6 9 tz7.44-3 ( ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) )