Metamath Proof Explorer

Theorem oe0rif

Description: Ordinal zero raised to any non-zero ordinal power is zero and zero to the zeroth power is one. Lemma 2.18 of Schloeder p. 6. (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion oe0rif ⊢ A ∈ On → ∅ ↑ 𝑜 A = if ∅ ∈ A ∅ 1 𝑜

Proof

Step Hyp Ref Expression
1 oe0m ⊢ A ∈ On → ∅ ↑ 𝑜 A = 1 𝑜 ∖ A
2 nel02 ⊢ A = ∅ → ¬ ∅ ∈ A
3 2 iffalsed ⊢ A = ∅ → if ∅ ∈ A ∅ 1 𝑜 = 1 𝑜
4 difeq2 ⊢ A = ∅ → 1 𝑜 ∖ A = 1 𝑜 ∖ ∅
5 dif0 ⊢ 1 𝑜 ∖ ∅ = 1 𝑜
6 4 5 eqtrdi ⊢ A = ∅ → 1 𝑜 ∖ A = 1 𝑜
7 3 6 eqtr4d ⊢ A = ∅ → if ∅ ∈ A ∅ 1 𝑜 = 1 𝑜 ∖ A
8 7 adantl ⊢ A ∈ On ∧ A = ∅ → if ∅ ∈ A ∅ 1 𝑜 = 1 𝑜 ∖ A
9 iftrue ⊢ ∅ ∈ A → if ∅ ∈ A ∅ 1 𝑜 = ∅
10 9 adantl ⊢ A ∈ On ∧ ∅ ∈ A → if ∅ ∈ A ∅ 1 𝑜 = ∅
11 eloni ⊢ A ∈ On → Ord ⁡ A
12 ordgt0ge1 ⊢ Ord ⁡ A → ∅ ∈ A ↔ 1 𝑜 ⊆ A
13 11 12 syl ⊢ A ∈ On → ∅ ∈ A ↔ 1 𝑜 ⊆ A
14 13 biimpa ⊢ A ∈ On ∧ ∅ ∈ A → 1 𝑜 ⊆ A
15 ssdif0 ⊢ 1 𝑜 ⊆ A ↔ 1 𝑜 ∖ A = ∅
16 14 15 sylib ⊢ A ∈ On ∧ ∅ ∈ A → 1 𝑜 ∖ A = ∅
17 10 16 eqtr4d ⊢ A ∈ On ∧ ∅ ∈ A → if ∅ ∈ A ∅ 1 𝑜 = 1 𝑜 ∖ A
18 on0eqel ⊢ A ∈ On → A = ∅ ∨ ∅ ∈ A
19 8 17 18 mpjaodan ⊢ A ∈ On → if ∅ ∈ A ∅ 1 𝑜 = 1 𝑜 ∖ A
20 1 19 eqtr4d ⊢ A ∈ On → ∅ ↑ 𝑜 A = if ∅ ∈ A ∅ 1 𝑜