Theorem oesuc

Description: Ordinal exponentiation with a successor exponent. Definition 8.30 of TakeutiZaring p. 67. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	oesuc	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o suc 𝐵 ) = ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		limon	⊢ Lim On
2		rdgsuc	⊢ ( 𝐵 ∈ On → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) )
3	1 2	oesuclem	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o suc 𝐵 ) = ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) )