# Metamath Proof Explorer

## Theorem oe1m

Description: Ordinal exponentiation with a mantissa of 1. Proposition 8.31(3) of TakeutiZaring p. 67. (Contributed by NM, 2-Jan-2005)

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

### Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{x}=\varnothing \to {1}_{𝑜}{↑}_{𝑜}{x}={1}_{𝑜}{↑}_{𝑜}\varnothing$
2 1 eqeq1d ${⊢}{x}=\varnothing \to \left({1}_{𝑜}{↑}_{𝑜}{x}={1}_{𝑜}↔{1}_{𝑜}{↑}_{𝑜}\varnothing ={1}_{𝑜}\right)$
3 oveq2 ${⊢}{x}={y}\to {1}_{𝑜}{↑}_{𝑜}{x}={1}_{𝑜}{↑}_{𝑜}{y}$
4 3 eqeq1d ${⊢}{x}={y}\to \left({1}_{𝑜}{↑}_{𝑜}{x}={1}_{𝑜}↔{1}_{𝑜}{↑}_{𝑜}{y}={1}_{𝑜}\right)$
5 oveq2 ${⊢}{x}=\mathrm{suc}{y}\to {1}_{𝑜}{↑}_{𝑜}{x}={1}_{𝑜}{↑}_{𝑜}\mathrm{suc}{y}$
6 5 eqeq1d ${⊢}{x}=\mathrm{suc}{y}\to \left({1}_{𝑜}{↑}_{𝑜}{x}={1}_{𝑜}↔{1}_{𝑜}{↑}_{𝑜}\mathrm{suc}{y}={1}_{𝑜}\right)$
7 oveq2 ${⊢}{x}={A}\to {1}_{𝑜}{↑}_{𝑜}{x}={1}_{𝑜}{↑}_{𝑜}{A}$
8 7 eqeq1d ${⊢}{x}={A}\to \left({1}_{𝑜}{↑}_{𝑜}{x}={1}_{𝑜}↔{1}_{𝑜}{↑}_{𝑜}{A}={1}_{𝑜}\right)$
9 1on ${⊢}{1}_{𝑜}\in \mathrm{On}$
10 oe0 ${⊢}{1}_{𝑜}\in \mathrm{On}\to {1}_{𝑜}{↑}_{𝑜}\varnothing ={1}_{𝑜}$
11 9 10 ax-mp ${⊢}{1}_{𝑜}{↑}_{𝑜}\varnothing ={1}_{𝑜}$
12 oesuc ${⊢}\left({1}_{𝑜}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {1}_{𝑜}{↑}_{𝑜}\mathrm{suc}{y}=\left({1}_{𝑜}{↑}_{𝑜}{y}\right){\cdot }_{𝑜}{1}_{𝑜}$
13 9 12 mpan ${⊢}{y}\in \mathrm{On}\to {1}_{𝑜}{↑}_{𝑜}\mathrm{suc}{y}=\left({1}_{𝑜}{↑}_{𝑜}{y}\right){\cdot }_{𝑜}{1}_{𝑜}$
14 oveq1 ${⊢}{1}_{𝑜}{↑}_{𝑜}{y}={1}_{𝑜}\to \left({1}_{𝑜}{↑}_{𝑜}{y}\right){\cdot }_{𝑜}{1}_{𝑜}={1}_{𝑜}{\cdot }_{𝑜}{1}_{𝑜}$
15 om1 ${⊢}{1}_{𝑜}\in \mathrm{On}\to {1}_{𝑜}{\cdot }_{𝑜}{1}_{𝑜}={1}_{𝑜}$
16 9 15 ax-mp ${⊢}{1}_{𝑜}{\cdot }_{𝑜}{1}_{𝑜}={1}_{𝑜}$
17 14 16 syl6eq ${⊢}{1}_{𝑜}{↑}_{𝑜}{y}={1}_{𝑜}\to \left({1}_{𝑜}{↑}_{𝑜}{y}\right){\cdot }_{𝑜}{1}_{𝑜}={1}_{𝑜}$
18 13 17 sylan9eq ${⊢}\left({y}\in \mathrm{On}\wedge {1}_{𝑜}{↑}_{𝑜}{y}={1}_{𝑜}\right)\to {1}_{𝑜}{↑}_{𝑜}\mathrm{suc}{y}={1}_{𝑜}$
19 18 ex ${⊢}{y}\in \mathrm{On}\to \left({1}_{𝑜}{↑}_{𝑜}{y}={1}_{𝑜}\to {1}_{𝑜}{↑}_{𝑜}\mathrm{suc}{y}={1}_{𝑜}\right)$
20 iuneq2 ${⊢}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{1}_{𝑜}{↑}_{𝑜}{y}={1}_{𝑜}\to \bigcup _{{y}\in {x}}\left({1}_{𝑜}{↑}_{𝑜}{y}\right)=\bigcup _{{y}\in {x}}{1}_{𝑜}$
21 vex ${⊢}{x}\in \mathrm{V}$
22 0lt1o ${⊢}\varnothing \in {1}_{𝑜}$
23 oelim ${⊢}\left(\left({1}_{𝑜}\in \mathrm{On}\wedge \left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\right)\wedge \varnothing \in {1}_{𝑜}\right)\to {1}_{𝑜}{↑}_{𝑜}{x}=\bigcup _{{y}\in {x}}\left({1}_{𝑜}{↑}_{𝑜}{y}\right)$
24 22 23 mpan2 ${⊢}\left({1}_{𝑜}\in \mathrm{On}\wedge \left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\right)\to {1}_{𝑜}{↑}_{𝑜}{x}=\bigcup _{{y}\in {x}}\left({1}_{𝑜}{↑}_{𝑜}{y}\right)$
25 9 24 mpan ${⊢}\left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\to {1}_{𝑜}{↑}_{𝑜}{x}=\bigcup _{{y}\in {x}}\left({1}_{𝑜}{↑}_{𝑜}{y}\right)$
26 21 25 mpan ${⊢}\mathrm{Lim}{x}\to {1}_{𝑜}{↑}_{𝑜}{x}=\bigcup _{{y}\in {x}}\left({1}_{𝑜}{↑}_{𝑜}{y}\right)$
27 26 eqeq1d ${⊢}\mathrm{Lim}{x}\to \left({1}_{𝑜}{↑}_{𝑜}{x}={1}_{𝑜}↔\bigcup _{{y}\in {x}}\left({1}_{𝑜}{↑}_{𝑜}{y}\right)={1}_{𝑜}\right)$
28 0ellim ${⊢}\mathrm{Lim}{x}\to \varnothing \in {x}$
29 ne0i ${⊢}\varnothing \in {x}\to {x}\ne \varnothing$
30 iunconst ${⊢}{x}\ne \varnothing \to \bigcup _{{y}\in {x}}{1}_{𝑜}={1}_{𝑜}$
31 28 29 30 3syl ${⊢}\mathrm{Lim}{x}\to \bigcup _{{y}\in {x}}{1}_{𝑜}={1}_{𝑜}$
32 31 eqeq2d ${⊢}\mathrm{Lim}{x}\to \left(\bigcup _{{y}\in {x}}\left({1}_{𝑜}{↑}_{𝑜}{y}\right)=\bigcup _{{y}\in {x}}{1}_{𝑜}↔\bigcup _{{y}\in {x}}\left({1}_{𝑜}{↑}_{𝑜}{y}\right)={1}_{𝑜}\right)$
33 27 32 bitr4d ${⊢}\mathrm{Lim}{x}\to \left({1}_{𝑜}{↑}_{𝑜}{x}={1}_{𝑜}↔\bigcup _{{y}\in {x}}\left({1}_{𝑜}{↑}_{𝑜}{y}\right)=\bigcup _{{y}\in {x}}{1}_{𝑜}\right)$
34 20 33 syl5ibr ${⊢}\mathrm{Lim}{x}\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{1}_{𝑜}{↑}_{𝑜}{y}={1}_{𝑜}\to {1}_{𝑜}{↑}_{𝑜}{x}={1}_{𝑜}\right)$
35 2 4 6 8 11 19 34 tfinds ${⊢}{A}\in \mathrm{On}\to {1}_{𝑜}{↑}_{𝑜}{A}={1}_{𝑜}$