Metamath Proof Explorer


Theorem rdgvalg

Description: Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion rdgvalg ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 df-rdg rec ( 𝐹 , 𝐴 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) )
2 1 tfr2a ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ 𝐵 ) ) )