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

Theorem df2o3 7740
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 7728 . 2 2𝑜 = suc 1𝑜
2 df-suc 5888 . 2 suc 1𝑜 = (1𝑜 ∪ {1𝑜})
3 df1o2 7739 . . . 4 1𝑜 = {∅}
43uneq1i 3904 . . 3 (1𝑜 ∪ {1𝑜}) = ({∅} ∪ {1𝑜})
5 df-pr 4322 . . 3 {∅, 1𝑜} = ({∅} ∪ {1𝑜})
64, 5eqtr4i 2783 . 2 (1𝑜 ∪ {1𝑜}) = {∅, 1𝑜}
71, 2, 63eqtri 2784 1 2𝑜 = {∅, 1𝑜}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1630  cun 3711  c0 4056  {csn 4319  {cpr 4321  suc csuc 5884  1𝑜c1o 7720  2𝑜c2o 7721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-v 3340  df-dif 3716  df-un 3718  df-nul 4057  df-pr 4322  df-suc 5888  df-1o 7727  df-2o 7728
This theorem is referenced by:  df2o2  7741  2oconcl  7750  map2xp  8293  1sdom  8326  cantnflem2  8758  xp2cda  9192  sdom2en01  9314  sadcf  15375  xpscfn  16419  xpscfv  16422  xpsfrnel  16423  xpsfeq  16424  xpsfrnel2  16425  xpsle  16441  setcepi  16937  efgi0  18331  efgi1  18332  vrgpf  18379  vrgpinv  18380  frgpuptinv  18382  frgpup2  18387  frgpup3lem  18388  frgpnabllem1  18474  dmdprdpr  18646  dprdpr  18647  xpstopnlem1  21812  xpstopnlem2  21814  xpsxmetlem  22383  xpsdsval  22385  xpsmet  22386  onint1  32752  pw2f1ocnv  38104  wepwsolem  38112  df3o2  38822  clsk1independent  38844
  Copyright terms: Public domain W3C validator