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 AOnA𝑜A=

Proof

Step Hyp Ref Expression
1 eloni AOnOrdA
2 ordgt0ge1 OrdAA1𝑜A
3 1 2 syl AOnA1𝑜A
4 ssdif0 1𝑜A1𝑜A=
5 oe0m AOn𝑜A=1𝑜A
6 5 eqeq1d AOn𝑜A=1𝑜A=
7 4 6 bitr4id AOn1𝑜A𝑜A=
8 3 7 bitrd AOnA𝑜A=