Metamath Proof Explorer


Theorem oe0m

Description: Value of zero raised to an ordinal. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oe0m A On 𝑜 A = 1 𝑜 A

Proof

Step Hyp Ref Expression
1 0elon On
2 oev On A On 𝑜 A = if = 1 𝑜 A rec x V x 𝑜 1 𝑜 A
3 1 2 mpan A On 𝑜 A = if = 1 𝑜 A rec x V x 𝑜 1 𝑜 A
4 eqid =
5 4 iftruei if = 1 𝑜 A rec x V x 𝑜 1 𝑜 A = 1 𝑜 A
6 3 5 eqtrdi A On 𝑜 A = 1 𝑜 A