Metamath Proof Explorer


Theorem oe0m1

Description: Ordinal exponentiation with zero base and nonzero exponent. Proposition 8.31(2) of TakeutiZaring p. 67 and its converse. (Contributed by NM, 5-Jan-2005)

Ref Expression
Assertion oe0m1 A On A 𝑜 A =

Proof

Step Hyp Ref Expression
1 eloni A On Ord A
2 ordgt0ge1 Ord A A 1 𝑜 A
3 1 2 syl A On A 1 𝑜 A
4 ssdif0 1 𝑜 A 1 𝑜 A =
5 oe0m A On 𝑜 A = 1 𝑜 A
6 5 eqeq1d A On 𝑜 A = 1 𝑜 A =
7 4 6 bitr4id A On 1 𝑜 A 𝑜 A =
8 3 7 bitrd A On A 𝑜 A =