# Metamath Proof Explorer

## Theorem 1oequni2o

Description: The ordinal number 1o is the predecessor of the ordinal number 2o . (Contributed by ML, 19-Oct-2020)

Ref Expression
Assertion 1oequni2o ${⊢}{1}_{𝑜}=\bigcup {2}_{𝑜}$

### Proof

Step Hyp Ref Expression
1 df-2o ${⊢}{2}_{𝑜}=\mathrm{suc}{1}_{𝑜}$
2 2on ${⊢}{2}_{𝑜}\in \mathrm{On}$
3 2on0 ${⊢}{2}_{𝑜}\ne \varnothing$
4 2onn ${⊢}{2}_{𝑜}\in \mathrm{\omega }$
5 nnlim ${⊢}{2}_{𝑜}\in \mathrm{\omega }\to ¬\mathrm{Lim}{2}_{𝑜}$
6 4 5 ax-mp ${⊢}¬\mathrm{Lim}{2}_{𝑜}$
7 onsucuni3 ${⊢}\left({2}_{𝑜}\in \mathrm{On}\wedge {2}_{𝑜}\ne \varnothing \wedge ¬\mathrm{Lim}{2}_{𝑜}\right)\to {2}_{𝑜}=\mathrm{suc}\bigcup {2}_{𝑜}$
8 2 3 6 7 mp3an ${⊢}{2}_{𝑜}=\mathrm{suc}\bigcup {2}_{𝑜}$
9 1 8 eqtr3i ${⊢}\mathrm{suc}{1}_{𝑜}=\mathrm{suc}\bigcup {2}_{𝑜}$
10 1on ${⊢}{1}_{𝑜}\in \mathrm{On}$
11 onuni ${⊢}{2}_{𝑜}\in \mathrm{On}\to \bigcup {2}_{𝑜}\in \mathrm{On}$
12 2 11 ax-mp ${⊢}\bigcup {2}_{𝑜}\in \mathrm{On}$
13 suc11 ${⊢}\left({1}_{𝑜}\in \mathrm{On}\wedge \bigcup {2}_{𝑜}\in \mathrm{On}\right)\to \left(\mathrm{suc}{1}_{𝑜}=\mathrm{suc}\bigcup {2}_{𝑜}↔{1}_{𝑜}=\bigcup {2}_{𝑜}\right)$
14 10 12 13 mp2an ${⊢}\mathrm{suc}{1}_{𝑜}=\mathrm{suc}\bigcup {2}_{𝑜}↔{1}_{𝑜}=\bigcup {2}_{𝑜}$
15 9 14 mpbi ${⊢}{1}_{𝑜}=\bigcup {2}_{𝑜}$