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

Theorem df2o3 6739
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 6727 . 2  |-  2o  =  suc  1o
2 df-suc 4589 . 2  |-  suc  1o  =  ( 1o  u.  { 1o } )
3 df1o2 6738 . . . 4  |-  1o  =  { (/) }
43uneq1i 3499 . . 3  |-  ( 1o  u.  { 1o }
)  =  ( {
(/) }  u.  { 1o } )
5 df-pr 3823 . . 3  |-  { (/) ,  1o }  =  ( { (/) }  u.  { 1o } )
64, 5eqtr4i 2461 . 2  |-  ( 1o  u.  { 1o }
)  =  { (/) ,  1o }
71, 2, 63eqtri 2462 1  |-  2o  =  { (/) ,  1o }
Colors of variables: wff set class
Syntax hints:    = wceq 1653    u. cun 3320   (/)c0 3630   {csn 3816   {cpr 3817   suc csuc 4585   1oc1o 6719   2oc2o 6720
This theorem is referenced by:  df2o2  6740  2oconcl  6749  map2xp  7279  1sdom  7313  cantnflem2  7648  xp2cda  8062  sdom2en01  8184  sadcf  12967  xpscfn  13786  xpscfv  13789  xpsfrnel  13790  xpsfeq  13791  xpsfrnel2  13792  xpsle  13808  setcepi  14245  efgi0  15354  efgi1  15355  vrgpf  15402  vrgpinv  15403  frgpuptinv  15405  frgpup2  15410  frgpup3lem  15411  frgpnabllem1  15486  dmdprdpr  15609  dprdpr  15610  xpstopnlem1  17843  xpstopnlem2  17845  xpsxmetlem  18411  xpsdsval  18413  xpsmet  18414  onint1  26201  pw2f1ocnv  27110  wepwsolem  27118
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325  df-un 3327  df-nul 3631  df-pr 3823  df-suc 4589  df-1o 6726  df-2o 6727
  Copyright terms: Public domain W3C validator