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

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 ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 rdgdmlim ⊢ Lim dom rec ( 𝐹 , 𝐴 )
2 limsuc ⊢ ( Lim dom rec ( 𝐹 , 𝐴 ) → ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) ↔ suc 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) ) )
3 1 2 ax-mp ⊢ ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) ↔ suc 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) )
4 eqid ⊢ ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) = ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) )
5 rdgvalg ⊢ ( 𝑦 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ 𝑦 ) ) )
6 rdgseg ⊢ ( 𝑦 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ↾ 𝑦 ) ∈ V )
7 rdgfun ⊢ Fun rec ( 𝐹 , 𝐴 )
8 funfn ⊢ ( Fun rec ( 𝐹 , 𝐴 ) ↔ rec ( 𝐹 , 𝐴 ) Fn dom rec ( 𝐹 , 𝐴 ) )
9 7 8 mpbi ⊢ rec ( 𝐹 , 𝐴 ) Fn dom rec ( 𝐹 , 𝐴 )
10 limord ⊢ ( Lim dom rec ( 𝐹 , 𝐴 ) → Ord dom rec ( 𝐹 , 𝐴 ) )
11 1 10 ax-mp ⊢ Ord dom rec ( 𝐹 , 𝐴 )
12 4 5 6 9 11 tz7.44-2 ⊢ ( suc 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )
13 3 12 sylbi ⊢ ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )