Step |
Hyp |
Ref |
Expression |
1 |
|
limom |
⊢ Lim ω |
2 |
|
frsuc |
⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ↾ ω ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ↾ ω ) ‘ 𝐵 ) ) ) |
3 |
|
peano2 |
⊢ ( 𝐵 ∈ ω → suc 𝐵 ∈ ω ) |
4 |
3
|
fvresd |
⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ↾ ω ) ‘ suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ suc 𝐵 ) ) |
5 |
|
fvres |
⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ↾ ω ) ‘ 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) |
6 |
5
|
fveq2d |
⊢ ( 𝐵 ∈ ω → ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ↾ ω ) ‘ 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) ) |
7 |
2 4 6
|
3eqtr3d |
⊢ ( 𝐵 ∈ ω → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) ) |
8 |
1 7
|
oesuclem |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ↑o suc 𝐵 ) = ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) ) |