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 
|- 3o = { (/) , 1o , 2o }

Proof

Step Hyp Ref Expression
1 df-3o 
 |-  3o = suc 2o
2 df2o3 
 |-  2o = { (/) , 1o }
3 2 uneq1i 
 |-  ( 2o u. { 2o } ) = ( { (/) , 1o } u. { 2o } )
4 df-suc 
 |-  suc 2o = ( 2o u. { 2o } )
5 df-tp 
 |-  { (/) , 1o , 2o } = ( { (/) , 1o } u. { 2o } )
6 3 4 5 3eqtr4i 
 |-  suc 2o = { (/) , 1o , 2o }
7 1 6 eqtri 
 |-  3o = { (/) , 1o , 2o }