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 ( 𝐹 , 𝐴 ) “ 𝐵 ) )