# Metamath Proof Explorer

## Theorem onesuc

Description: Exponentiation with a successor exponent. Definition 8.30 of TakeutiZaring p. 67. (Contributed by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion onesuc ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to {A}{↑}_{𝑜}\mathrm{suc}{B}=\left({A}{↑}_{𝑜}{B}\right){\cdot }_{𝑜}{A}$

### Proof

Step Hyp Ref Expression
1 limom ${⊢}\mathrm{Lim}\mathrm{\omega }$
2 frsuc ${⊢}{B}\in \mathrm{\omega }\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{B}\right)=\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right)\left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)↾}_{\mathrm{\omega }}\right)\left({B}\right)\right)$
3 peano2 ${⊢}{B}\in \mathrm{\omega }\to \mathrm{suc}{B}\in \mathrm{\omega }$
4 3 fvresd ${⊢}{B}\in \mathrm{\omega }\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{B}\right)=\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left(\mathrm{suc}{B}\right)$
5 fvres ${⊢}{B}\in \mathrm{\omega }\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)↾}_{\mathrm{\omega }}\right)\left({B}\right)=\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({B}\right)$
6 5 fveq2d ${⊢}{B}\in \mathrm{\omega }\to \left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right)\left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)↾}_{\mathrm{\omega }}\right)\left({B}\right)\right)=\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right)\left(\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({B}\right)\right)$
7 2 4 6 3eqtr3d ${⊢}{B}\in \mathrm{\omega }\to \mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left(\mathrm{suc}{B}\right)=\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right)\left(\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left({B}\right)\right)$
8 1 7 oesuclem ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to {A}{↑}_{𝑜}\mathrm{suc}{B}=\left({A}{↑}_{𝑜}{B}\right){\cdot }_{𝑜}{A}$