Metamath Proof Explorer


Theorem rdglim

Description: The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 23-Apr-1995) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion rdglim ( ( 𝐵𝐶 ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 limelon ( ( 𝐵𝐶 ∧ Lim 𝐵 ) → 𝐵 ∈ On )
2 rdgfnon rec ( 𝐹 , 𝐴 ) Fn On
3 fndm ( rec ( 𝐹 , 𝐴 ) Fn On → dom rec ( 𝐹 , 𝐴 ) = On )
4 2 3 ax-mp dom rec ( 𝐹 , 𝐴 ) = On
5 1 4 eleqtrrdi ( ( 𝐵𝐶 ∧ Lim 𝐵 ) → 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) )
6 rdglimg ( ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) )
7 5 6 sylancom ( ( 𝐵𝐶 ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) )