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	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ ( ∅ ↑o 𝐴 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
2		ordgt0ge1	⊢ ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴 ) )
4		ssdif0	⊢ ( 1o ⊆ 𝐴 ↔ ( 1o ∖ 𝐴 ) = ∅ )
5		oe0m	⊢ ( 𝐴 ∈ On → ( ∅ ↑o 𝐴 ) = ( 1o ∖ 𝐴 ) )
6	5	eqeq1d	⊢ ( 𝐴 ∈ On → ( ( ∅ ↑o 𝐴 ) = ∅ ↔ ( 1o ∖ 𝐴 ) = ∅ ) )
7	4 6	bitr4id	⊢ ( 𝐴 ∈ On → ( 1o ⊆ 𝐴 ↔ ( ∅ ↑o 𝐴 ) = ∅ ) )
8	3 7	bitrd	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ ( ∅ ↑o 𝐴 ) = ∅ ) )