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

Theorem df2o3 7728
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 7715 . 2 2𝑜 = suc 1𝑜
2 df-suc 5873 . 2 suc 1𝑜 = (1𝑜 ∪ {1𝑜})
3 df1o2 7727 . . . 4 1𝑜 = {∅}
43uneq1i 3915 . . 3 (1𝑜 ∪ {1𝑜}) = ({∅} ∪ {1𝑜})
5 df-pr 4320 . . 3 {∅, 1𝑜} = ({∅} ∪ {1𝑜})
64, 5eqtr4i 2796 . 2 (1𝑜 ∪ {1𝑜}) = {∅, 1𝑜}
71, 2, 63eqtri 2797 1 2𝑜 = {∅, 1𝑜}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  cun 3722  c0 4064  {csn 4317  {cpr 4319  suc csuc 5869  1𝑜c1o 7707  2𝑜c2o 7708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3727  df-un 3729  df-nul 4065  df-pr 4320  df-suc 5873  df-1o 7714  df-2o 7715
This theorem is referenced by:  df2o2  7729  2oconcl  7738  map2xp  8287  1sdom  8320  cantnflem2  8752  xp2cda  9205  sdom2en01  9327  sadcf  15384  xpscfn  16428  xpscfv  16431  xpsfrnel  16432  xpsfeq  16433  xpsfrnel2  16434  xpsle  16450  setcepi  16946  efgi0  18341  efgi1  18342  vrgpf  18389  vrgpinv  18390  frgpuptinv  18392  frgpup2  18397  frgpup3lem  18398  frgpnabllem1  18484  dmdprdpr  18657  dprdpr  18658  xpstopnlem1  21834  xpstopnlem2  21836  xpsxmetlem  22405  xpsdsval  22407  xpsmet  22408  onint1  32786  pw2f1ocnv  38131  wepwsolem  38139  df3o2  38849  clsk1independent  38871
  Copyright terms: Public domain W3C validator