Theorem df2o3 6576

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

Assertion

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

Proof of Theorem df2o3

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

Syntax hints:   = wceq 1395   u. cun 3195   (/)c0 3491   {csn 3666   {cpr 3667   suc csuc 4456   1oc1o 6555   2oc2o 6556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-dif 3199  df-un 3201  df-nul 3492  df-pr 3673  df-suc 4462  df-1o 6562  df-2o 6563

This theorem is referenced by:  df2o2  6577  2oconcl  6585  0lt2o  6587  1lt2o  6588  el2oss1o  6589  rex2dom  6971  en2  6973  en2eqpr  7069  nninfisol  7300  finomni  7307  exmidomniim  7308  exmidomni  7309  ismkvnex  7322  nninfwlpoimlemginf  7343  pr2cv1  7368  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  xp2dju  7397  pw1nel3  7416  sucpw1nel3  7418  nninfctlemfo  12561  unct  13013  fnpr2o  13372  fnpr2ob  13373  fvprif  13376  xpsfrnel  13377  xpsfeq  13378  2o01f  16358  2omap  16359  nninfalllem1  16374  nninfall  16375  nninfsellemqall  16381  nninfomnilem  16384  nnnninfex  16388  nninfnfiinf  16389