This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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