Theorem df2o3 6421

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 6408	. 2 |- 2o = suc 1o
2		df-suc 4365	. 2 |- suc 1o = ( 1o u. { 1o } )
3		df1o2 6420	. . . 4 |- 1o = { (/) }
4	3	uneq1i 3283	. . 3 |- ( 1o u. { 1o } ) = ( { (/) } u. { 1o } )
5		df-pr 3596	. . 3 |- { (/) , 1o } = ( { (/) } u. { 1o } )
6	4, 5	eqtr4i 2199	. 2 |- ( 1o u. { 1o } ) = { (/) , 1o }
7	1, 2, 6	3eqtri 2200	1 |- 2o = { (/) , 1o }

Syntax hints:   = wceq 1353   u. cun 3125   (/)c0 3420   {csn 3589   {cpr 3590   suc csuc 4359   1oc1o 6400   2oc2o 6401

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 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-dif 3129  df-un 3131  df-nul 3421  df-pr 3596  df-suc 4365  df-1o 6407  df-2o 6408

This theorem is referenced by:  df2o2  6422  2oconcl  6430  0lt2o  6432  1lt2o  6433  el2oss1o  6434  en2eqpr  6897  nninfisol  7121  finomni  7128  exmidomniim  7129  exmidomni  7130  ismkvnex  7143  nninfwlpoimlemginf  7164  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  xp2dju  7204  pw1nel3  7220  sucpw1nel3  7222  unct  12408  2o01f  14286  nninfalllem1  14298  nninfall  14299  nninfsellemqall  14305  nninfomnilem  14308