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

Metamath Proof Explorer

Theorem rdgsuc

Description: The value of the recursive definition generator at a successor. (Contributed by NM, 23-Apr-1995) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion rdgsuc ⊢ B ∈ On → rec ⁡ F A ⁡ suc ⁡ B = F ⁡ rec ⁡ F A ⁡ B

Proof

Step Hyp Ref Expression
1 rdgfnon ⊢ rec ⁡ F A Fn On
2 1 fndmi ⊢ dom ⁡ rec ⁡ F A = On
3 2 eleq2i ⊢ B ∈ dom ⁡ rec ⁡ F A ↔ B ∈ On
4 rdgsucg ⊢ B ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ⁡ suc ⁡ B = F ⁡ rec ⁡ F A ⁡ B
5 3 4 sylbir ⊢ B ∈ On → rec ⁡ F A ⁡ suc ⁡ B = F ⁡ rec ⁡ F A ⁡ B