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