Metamath Proof Explorer


Theorem oe0

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

Ref Expression
Assertion oe0 A On A 𝑜 = 1 𝑜

Proof

Step Hyp Ref Expression
1 oveq1 A = A 𝑜 = 𝑜
2 oe0m0 𝑜 = 1 𝑜
3 1 2 syl6eq A = A 𝑜 = 1 𝑜
4 3 adantl A On A = A 𝑜 = 1 𝑜
5 0elon On
6 oevn0 A On On A A 𝑜 = rec x V x 𝑜 A 1 𝑜
7 5 6 mpanl2 A On A A 𝑜 = rec x V x 𝑜 A 1 𝑜
8 1oex 1 𝑜 V
9 8 rdg0 rec x V x 𝑜 A 1 𝑜 = 1 𝑜
10 7 9 syl6eq A On A A 𝑜 = 1 𝑜
11 10 adantll A On A On A A 𝑜 = 1 𝑜
12 4 11 oe0lem A On A On A 𝑜 = 1 𝑜
13 12 anidms A On A 𝑜 = 1 𝑜