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 ∅ ∈ On
2 oe0m ( ∅ ∈ On → ( ∅ ↑o ∅ ) = ( 1o ∖ ∅ ) )
3 1 2 ax-mp ( ∅ ↑o ∅ ) = ( 1o ∖ ∅ )
4 dif0 ( 1o ∖ ∅ ) = 1o
5 3 4 eqtri ( ∅ ↑o ∅ ) = 1o