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

Theorem df2o3 7518
Description: Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
df2o3 2𝑜 = {∅, 1𝑜}

Proof of Theorem df2o3
StepHypRef Expression
1 df-2o 7506 . 2 2𝑜 = suc 1𝑜
2 df-suc 5688 . 2 suc 1𝑜 = (1𝑜 ∪ {1𝑜})
3 df1o2 7517 . . . 4 1𝑜 = {∅}
43uneq1i 3741 . . 3 (1𝑜 ∪ {1𝑜}) = ({∅} ∪ {1𝑜})
5 df-pr 4151 . . 3 {∅, 1𝑜} = ({∅} ∪ {1𝑜})
64, 5eqtr4i 2646 . 2 (1𝑜 ∪ {1𝑜}) = {∅, 1𝑜}
71, 2, 63eqtri 2647 1 2𝑜 = {∅, 1𝑜}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  cun 3553  c0 3891  {csn 4148  {cpr 4150  suc csuc 5684  1𝑜c1o 7498  2𝑜c2o 7499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-dif 3558  df-un 3560  df-nul 3892  df-pr 4151  df-suc 5688  df-1o 7505  df-2o 7506
This theorem is referenced by:  df2o2  7519  2oconcl  7528  map2xp  8074  1sdom  8107  cantnflem2  8531  xp2cda  8946  sdom2en01  9068  sadcf  15099  xpscfn  16140  xpscfv  16143  xpsfrnel  16144  xpsfeq  16145  xpsfrnel2  16146  xpsle  16162  setcepi  16659  efgi0  18054  efgi1  18055  vrgpf  18102  vrgpinv  18103  frgpuptinv  18105  frgpup2  18110  frgpup3lem  18111  frgpnabllem1  18197  dmdprdpr  18369  dprdpr  18370  xpstopnlem1  21522  xpstopnlem2  21524  xpsxmetlem  22094  xpsdsval  22096  xpsmet  22097  onint1  32090  pw2f1ocnv  37084  wepwsolem  37092  df3o2  37804  clsk1independent  37826
  Copyright terms: Public domain W3C validator