MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df2o3 Unicode version

Theorem df2o3 6492
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
StepHypRef Expression
1 df-2o 6480 . 2  |-  2o  =  suc  1o
2 df-suc 4398 . 2  |-  suc  1o  =  ( 1o  u.  { 1o } )
3 df1o2 6491 . . . 4  |-  1o  =  { (/) }
43uneq1i 3325 . . 3  |-  ( 1o  u.  { 1o }
)  =  ( {
(/) }  u.  { 1o } )
5 df-pr 3647 . . 3  |-  { (/) ,  1o }  =  ( { (/) }  u.  { 1o } )
64, 5eqtr4i 2306 . 2  |-  ( 1o  u.  { 1o }
)  =  { (/) ,  1o }
71, 2, 63eqtri 2307 1  |-  2o  =  { (/) ,  1o }
Colors of variables: wff set class
Syntax hints:    = wceq 1623    u. cun 3150   (/)c0 3455   {csn 3640   {cpr 3641   suc csuc 4394   1oc1o 6472   2oc2o 6473
This theorem is referenced by:  df2o2  6493  2oconcl  6502  map2xp  7031  1sdom  7065  cantnflem2  7392  xp2cda  7806  sdom2en01  7928  sadcf  12644  xpscfn  13461  xpscfv  13464  xpsfrnel  13465  xpsfeq  13466  xpsfrnel2  13467  xpsle  13483  setcepi  13920  efgi0  15029  efgi1  15030  vrgpf  15077  vrgpinv  15078  frgpuptinv  15080  frgpup2  15085  frgpup3lem  15086  frgpnabllem1  15161  dmdprdpr  15284  dprdpr  15285  xpstopnlem1  17500  xpstopnlem2  17502  xpsxmetlem  17943  xpsdsval  17945  xpsmet  17946  onint1  24299  pw2f1ocnv  26542  wepwsolem  26550
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-un 3157  df-nul 3456  df-pr 3647  df-suc 4398  df-1o 6479  df-2o 6480
  Copyright terms: Public domain W3C validator