Metamath Proof Explorer


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 ( 𝐹 , 𝐴 ) ‘ 𝑥 ) )