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𝑜