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

Metamath Proof Explorer

Theorem rdgdmlim

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

Ref Expression
Assertion rdgdmlim ⊢ Lim ⁡ dom ⁡ rec ⁡ F A

Proof

Step Hyp Ref Expression
1 df-rdg ⊢ rec ⁡ F A = recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
2 1 tfr1a ⊢ Fun ⁡ rec ⁡ F A ∧ Lim ⁡ dom ⁡ rec ⁡ F A
3 2 simpri ⊢ Lim ⁡ dom ⁡ rec ⁡ F A