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 ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) ) |