Metamath Proof Explorer

Theorem df2o3

Description: Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion df2o3 
|- 2o = { (/) , 1o }

Proof

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