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

Theorem df2o3 6508
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 6496 . 2  |-  2o  =  suc  1o
2 df-suc 4414 . 2  |-  suc  1o  =  ( 1o  u.  { 1o } )
3 df1o2 6507 . . . 4  |-  1o  =  { (/) }
43uneq1i 3338 . . 3  |-  ( 1o  u.  { 1o }
)  =  ( {
(/) }  u.  { 1o } )
5 df-pr 3660 . . 3  |-  { (/) ,  1o }  =  ( { (/) }  u.  { 1o } )
64, 5eqtr4i 2319 . 2  |-  ( 1o  u.  { 1o }
)  =  { (/) ,  1o }
71, 2, 63eqtri 2320 1  |-  2o  =  { (/) ,  1o }
Colors of variables: wff set class
Syntax hints:    = wceq 1632    u. cun 3163   (/)c0 3468   {csn 3653   {cpr 3654   suc csuc 4410   1oc1o 6488   2oc2o 6489
This theorem is referenced by:  df2o2  6509  2oconcl  6518  map2xp  7047  1sdom  7081  cantnflem2  7408  xp2cda  7822  sdom2en01  7944  sadcf  12660  xpscfn  13477  xpscfv  13480  xpsfrnel  13481  xpsfeq  13482  xpsfrnel2  13483  xpsle  13499  setcepi  13936  efgi0  15045  efgi1  15046  vrgpf  15093  vrgpinv  15094  frgpuptinv  15096  frgpup2  15101  frgpup3lem  15102  frgpnabllem1  15177  dmdprdpr  15300  dprdpr  15301  xpstopnlem1  17516  xpstopnlem2  17518  xpsxmetlem  17959  xpsdsval  17961  xpsmet  17962  onint1  24960  pw2f1ocnv  27233  wepwsolem  27241
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-un 3170  df-nul 3469  df-pr 3660  df-suc 4414  df-1o 6495  df-2o 6496
  Copyright terms: Public domain W3C validator