Metamath Proof Explorer


Theorem df3o2

Description: Ordinal 3 is the unordered triple containing ordinals 0, 1, and 2. (Contributed by RP, 8-Jul-2021)

Ref Expression
Assertion df3o2 3𝑜=1𝑜2𝑜

Proof

Step Hyp Ref Expression
1 df-3o 3𝑜=suc2𝑜
2 df2o3 2𝑜=1𝑜
3 2 uneq1i 2𝑜2𝑜=1𝑜2𝑜
4 df-suc suc2𝑜=2𝑜2𝑜
5 df-tp 1𝑜2𝑜=1𝑜2𝑜
6 3 4 5 3eqtr4i suc2𝑜=1𝑜2𝑜
7 1 6 eqtri 3𝑜=1𝑜2𝑜