# Metamath Proof Explorer

## Theorem oe1

Description: Ordinal exponentiation with an exponent of 1. (Contributed by NM, 2-Jan-2005)

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

### Proof

Step Hyp Ref Expression
1 df-1o ${⊢}{1}_{𝑜}=\mathrm{suc}\varnothing$
2 1 oveq2i ${⊢}{A}{↑}_{𝑜}{1}_{𝑜}={A}{↑}_{𝑜}\mathrm{suc}\varnothing$
3 peano1 ${⊢}\varnothing \in \mathrm{\omega }$
4 onesuc ${⊢}\left({A}\in \mathrm{On}\wedge \varnothing \in \mathrm{\omega }\right)\to {A}{↑}_{𝑜}\mathrm{suc}\varnothing =\left({A}{↑}_{𝑜}\varnothing \right){\cdot }_{𝑜}{A}$
5 3 4 mpan2 ${⊢}{A}\in \mathrm{On}\to {A}{↑}_{𝑜}\mathrm{suc}\varnothing =\left({A}{↑}_{𝑜}\varnothing \right){\cdot }_{𝑜}{A}$
6 2 5 syl5eq ${⊢}{A}\in \mathrm{On}\to {A}{↑}_{𝑜}{1}_{𝑜}=\left({A}{↑}_{𝑜}\varnothing \right){\cdot }_{𝑜}{A}$
7 oe0 ${⊢}{A}\in \mathrm{On}\to {A}{↑}_{𝑜}\varnothing ={1}_{𝑜}$
8 7 oveq1d ${⊢}{A}\in \mathrm{On}\to \left({A}{↑}_{𝑜}\varnothing \right){\cdot }_{𝑜}{A}={1}_{𝑜}{\cdot }_{𝑜}{A}$
9 om1r ${⊢}{A}\in \mathrm{On}\to {1}_{𝑜}{\cdot }_{𝑜}{A}={A}$
10 6 8 9 3eqtrd ${⊢}{A}\in \mathrm{On}\to {A}{↑}_{𝑜}{1}_{𝑜}={A}$