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

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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ↑o suc 𝐵 ) = ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) )

Proof

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 𝐴 ) )