# Metamath Proof Explorer

## Theorem df3o3

Description: Ordinal 3 , fully expanded. (Contributed by RP, 8-Jul-2021)

Ref Expression
Assertion df3o3 ${⊢}{3}_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\},\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}$

### Proof

Step Hyp Ref Expression
1 df-3o ${⊢}{3}_{𝑜}=\mathrm{suc}{2}_{𝑜}$
2 df2o2 ${⊢}{2}_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$
3 2 sneqi ${⊢}\left\{{2}_{𝑜}\right\}=\left\{\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}$
4 2 3 uneq12i ${⊢}{2}_{𝑜}\cup \left\{{2}_{𝑜}\right\}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}\cup \left\{\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}$
5 df-suc ${⊢}\mathrm{suc}{2}_{𝑜}={2}_{𝑜}\cup \left\{{2}_{𝑜}\right\}$
6 df-tp ${⊢}\left\{\varnothing ,\left\{\varnothing \right\},\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}\cup \left\{\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}$
7 4 5 6 3eqtr4i ${⊢}\mathrm{suc}{2}_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\},\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}$
8 1 7 eqtri ${⊢}{3}_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\},\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right\}$