Metamath Proof Explorer

Theorem rdglimg

Description: The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 16-Nov-2014)

Ref Expression
Assertion rdglimg ⊢ B ∈ dom ⁡ rec ⁡ F A ∧ Lim ⁡ B → rec ⁡ F A ⁡ B = ⋃ rec ⁡ F A B

Proof

Step Hyp Ref Expression
1 eqid ⊢ x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x = x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x
2 rdgvalg ⊢ y ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ⁡ y = x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x ⁡ rec ⁡ F A ↾ y
3 rdgseg ⊢ y ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ↾ y ∈ V
4 rdgfun ⊢ Fun ⁡ rec ⁡ F A
5 funfn ⊢ Fun ⁡ rec ⁡ F A ↔ rec ⁡ F A Fn dom ⁡ rec ⁡ F A
6 4 5 mpbi ⊢ rec ⁡ F A Fn dom ⁡ rec ⁡ F A
7 rdgdmlim ⊢ Lim ⁡ dom ⁡ rec ⁡ F A
8 limord ⊢ Lim ⁡ dom ⁡ rec ⁡ F A → Ord ⁡ dom ⁡ rec ⁡ F A
9 7 8 ax-mp ⊢ Ord ⁡ dom ⁡ rec ⁡ F A
10 1 2 3 6 9 tz7.44-3 ⊢ B ∈ dom ⁡ rec ⁡ F A ∧ Lim ⁡ B → rec ⁡ F A ⁡ B = ⋃ rec ⁡ F A B