This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ B ∈ C ∧ Lim ⁡ B → rec ⁡ F A ⁡ B = ⋃ x ∈ B rec ⁡ F A ⁡ x

Proof

Step Hyp Ref Expression
1 rdglim2 ⊢ B ∈ C ∧ Lim ⁡ B → rec ⁡ F A ⁡ B = ⋃ y | ∃ x ∈ B y = rec ⁡ F A ⁡ x
2 fvex ⊢ rec ⁡ F A ⁡ x ∈ V
3 2 dfiun2 ⊢ ⋃ x ∈ B rec ⁡ F A ⁡ x = ⋃ y | ∃ x ∈ B y = rec ⁡ F A ⁡ x
4 1 3 eqtr4di ⊢ B ∈ C ∧ Lim ⁡ B → rec ⁡ F A ⁡ B = ⋃ x ∈ B rec ⁡ F A ⁡ x