Metamath Proof Explorer

Theorem oe0m0

Description: Ordinal exponentiation with zero base and zero exponent. Proposition 8.31 of TakeutiZaring p. 67. (Contributed by NM, 31-Dec-2004)

Ref Expression
Assertion oe0m0 
|- ( (/) ^o (/) ) = 1o

Proof

Step Hyp Ref Expression
1 0elon 
 |-  (/) e. On
2 oe0m 
 |-  ( (/) e. On -> ( (/) ^o (/) ) = ( 1o \ (/) ) )
3 1 2 ax-mp 
 |-  ( (/) ^o (/) ) = ( 1o \ (/) )
4 dif0 
 |-  ( 1o \ (/) ) = 1o
5 3 4 eqtri 
 |-  ( (/) ^o (/) ) = 1o