# Metamath Proof Explorer

## Theorem oe0

Description: Ordinal exponentiation with zero exponent. Definition 8.30 of TakeutiZaring p. 67. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oe0 ${⊢}{A}\in \mathrm{On}\to {A}{↑}_{𝑜}\varnothing ={1}_{𝑜}$

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{A}=\varnothing \to {A}{↑}_{𝑜}\varnothing =\varnothing {↑}_{𝑜}\varnothing$
2 oe0m0 ${⊢}\varnothing {↑}_{𝑜}\varnothing ={1}_{𝑜}$
3 1 2 syl6eq ${⊢}{A}=\varnothing \to {A}{↑}_{𝑜}\varnothing ={1}_{𝑜}$
4 3 adantl ${⊢}\left({A}\in \mathrm{On}\wedge {A}=\varnothing \right)\to {A}{↑}_{𝑜}\varnothing ={1}_{𝑜}$
5 0elon ${⊢}\varnothing \in \mathrm{On}$
6 oevn0 ${⊢}\left(\left({A}\in \mathrm{On}\wedge \varnothing \in \mathrm{On}\right)\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}\varnothing =\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left(\varnothing \right)$
7 5 6 mpanl2 ${⊢}\left({A}\in \mathrm{On}\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}\varnothing =\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left(\varnothing \right)$
8 1oex ${⊢}{1}_{𝑜}\in \mathrm{V}$
9 8 rdg0 ${⊢}\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{\cdot }_{𝑜}{A}\right),{1}_{𝑜}\right)\left(\varnothing \right)={1}_{𝑜}$
10 7 9 syl6eq ${⊢}\left({A}\in \mathrm{On}\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}\varnothing ={1}_{𝑜}$
11 10 adantll ${⊢}\left(\left({A}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\wedge \varnothing \in {A}\right)\to {A}{↑}_{𝑜}\varnothing ={1}_{𝑜}$
12 4 11 oe0lem ${⊢}\left({A}\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\to {A}{↑}_{𝑜}\varnothing ={1}_{𝑜}$
13 12 anidms ${⊢}{A}\in \mathrm{On}\to {A}{↑}_{𝑜}\varnothing ={1}_{𝑜}$