Description: Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 8-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | rdgval | ⊢ ( 𝐵 ∈ On → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ 𝐵 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rdg | ⊢ rec ( 𝐹 , 𝐴 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) | |
2 | 1 | tfr2 | ⊢ ( 𝐵 ∈ On → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ 𝐵 ) ) ) |