Theorem rdglim2a

Description: The value of the recursive definition generator at a limit ordinal, in terms of indexed union of all smaller values. (Contributed by NM, 28-Jun-1998)

	Ref	Expression
Assertion	rdglim2a	⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		rdglim2	⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) } )
2		fvex	⊢ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ∈ V
3	2	dfiun2	⊢ ∪ 𝑥 ∈ 𝐵 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) }
4	1 3	eqtr4di	⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) )