Theorem df2o3 6929

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 6917	. 2 |- 2o = suc 1o
2		df-suc 4721	. 2 |- suc 1o = ( 1o u. { 1o } )
3		df1o2 6928	. . . 4 |- 1o = { (/) }
4	3	uneq1i 3503	. . 3 |- ( 1o u. { 1o } ) = ( { (/) } u. { 1o } )
5		df-pr 3877	. . 3 |- { (/) , 1o } = ( { (/) } u. { 1o } )
6	4, 5	eqtr4i 2464	. 2 |- ( 1o u. { 1o } ) = { (/) , 1o }
7	1, 2, 6	3eqtri 2465	1 |- 2o = { (/) , 1o }

Syntax hints:   = wceq 1364   u. cun 3323   (/)c0 3634   {csn 3874   {cpr 3876   suc csuc 4717   1oc1o 6909   2oc2o 6910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-dif 3328  df-un 3330  df-nul 3635  df-pr 3877  df-suc 4721  df-1o 6916  df-2o 6917

This theorem is referenced by:  df2o2  6930  2oconcl  6939  map2xp  7477  1sdom  7511  cantnflem2  7894  xp2cda  8345  sdom2en01  8467  sadcf  13645  xpscfn  14493  xpscfv  14496  xpsfrnel  14497  xpsfeq  14498  xpsfrnel2  14499  xpsle  14515  setcepi  14952  efgi0  16210  efgi1  16211  vrgpf  16258  vrgpinv  16259  frgpuptinv  16261  frgpup2  16266  frgpup3lem  16267  frgpnabllem1  16344  dmdprdpr  16538  dprdpr  16539  xpstopnlem1  19282  xpstopnlem2  19284  xpsxmetlem  19854  xpsdsval  19856  xpsmet  19857  onint1  28209  pw2f1ocnv  29295  wepwsolem  29303