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