Metamath Proof Explorer

Theorem oesuc

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

Ref Expression
Assertion oesuc ⊢ A ∈ On ∧ B ∈ On → A ↑ 𝑜 suc ⁡ B = A ↑ 𝑜 B ⋅ 𝑜 A

Proof

Step Hyp Ref Expression
1 limon ⊢ Lim ⁡ On
2 rdgsuc ⊢ B ∈ On → rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ suc ⁡ B = x ∈ V ⟼ x ⋅ 𝑜 A ⁡ rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B
3 1 2 oesuclem ⊢ A ∈ On ∧ B ∈ On → A ↑ 𝑜 suc ⁡ B = A ↑ 𝑜 B ⋅ 𝑜 A