Metamath Proof Explorer

Theorem rdgsucg

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

Ref Expression
Assertion rdgsucg ⊢ B ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ⁡ suc ⁡ B = F ⁡ rec ⁡ F A ⁡ B

Proof

Step Hyp Ref Expression
1 rdgdmlim ⊢ Lim ⁡ dom ⁡ rec ⁡ F A
2 limsuc ⊢ Lim ⁡ dom ⁡ rec ⁡ F A → B ∈ dom ⁡ rec ⁡ F A ↔ suc ⁡ B ∈ dom ⁡ rec ⁡ F A
3 1 2 ax-mp ⊢ B ∈ dom ⁡ rec ⁡ F A ↔ suc ⁡ B ∈ dom ⁡ rec ⁡ F A
4 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
5 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
6 rdgseg ⊢ y ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ↾ y ∈ V
7 rdgfun ⊢ Fun ⁡ rec ⁡ F A
8 funfn ⊢ Fun ⁡ rec ⁡ F A ↔ rec ⁡ F A Fn dom ⁡ rec ⁡ F A
9 7 8 mpbi ⊢ rec ⁡ F A Fn dom ⁡ rec ⁡ F A
10 limord ⊢ Lim ⁡ dom ⁡ rec ⁡ F A → Ord ⁡ dom ⁡ rec ⁡ F A
11 1 10 ax-mp ⊢ Ord ⁡ dom ⁡ rec ⁡ F A
12 4 5 6 9 11 tz7.44-2 ⊢ suc ⁡ B ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ⁡ suc ⁡ B = F ⁡ rec ⁡ F A ⁡ B
13 3 12 sylbi ⊢ B ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ⁡ suc ⁡ B = F ⁡ rec ⁡ F A ⁡ B