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

Metamath Proof Explorer

Theorem frsuc

Description: The successor value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion frsuc ( 𝐵 ∈ ω → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 rdgdmlim ⊢ Lim dom rec ( 𝐹 , 𝐴 )
2 limomss ⊢ ( Lim dom rec ( 𝐹 , 𝐴 ) → ω ⊆ dom rec ( 𝐹 , 𝐴 ) )
3 1 2 ax-mp ⊢ ω ⊆ dom rec ( 𝐹 , 𝐴 )
4 3 sseli ⊢ ( 𝐵 ∈ ω → 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) )
5 rdgsucg ⊢ ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )
6 4 5 syl ⊢ ( 𝐵 ∈ ω → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )
7 peano2b ⊢ ( 𝐵 ∈ ω ↔ suc 𝐵 ∈ ω )
8 fvres ⊢ ( suc 𝐵 ∈ ω → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) )
9 7 8 sylbi ⊢ ( 𝐵 ∈ ω → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝐵 ) )
10 fvres ⊢ ( 𝐵 ∈ ω → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝐵 ) = ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) )
11 10 fveq2d ⊢ ( 𝐵 ∈ ω → ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )
12 6 9 11 3eqtr4d ⊢ ( 𝐵 ∈ ω → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) )