Metamath Proof Explorer


Theorem df3o3

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

Ref Expression
Assertion df3o3 3 𝑜 =

Proof

Step Hyp Ref Expression
1 df-3o 3 𝑜 = suc 2 𝑜
2 df2o2 2 𝑜 =
3 2 sneqi 2 𝑜 =
4 2 3 uneq12i 2 𝑜 2 𝑜 =
5 df-suc suc 2 𝑜 = 2 𝑜 2 𝑜
6 df-tp =
7 4 5 6 3eqtr4i suc 2 𝑜 =
8 1 7 eqtri 3 𝑜 =