Metamath Proof Explorer

Theorem oe0m1

Description: Ordinal exponentiation with zero base and nonzero exponent. Proposition 8.31(2) of TakeutiZaring p. 67 and its converse. Definition 2.6 of Schloeder p. 4. (Contributed by NM, 5-Jan-2005)

Ref Expression
Assertion oe0m1 ⊢ A ∈ On → ∅ ∈ A ↔ ∅ ↑ 𝑜 A = ∅

Proof

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