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

Metamath Proof Explorer

Theorem rdgfun

Description: The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion rdgfun ⊢ Fun ⁡ 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 simpli ⊢ Fun ⁡ rec ⁡ F A