Theorem df2o3 8492

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

Step	Hyp	Ref	Expression
1		df-2o 8485	. 2 ⊢ 2o = suc 1o
2		df-suc 6371	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8491	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4162	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4587	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2786	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2787	1 ⊢ 2o = {∅, 1o}

This proof depends on syntax axioms:   = wceq 1569   ∪ cun 4148  ∅c0 4277  {csn 4584  {cpr 4586  suc csuc 6367  1_oc1o 8477  2_oc2o 8478

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4046  df-un 4150  df-nul 4278  df-pr 4587  df-suc 6371  df-1o 8484  df-2o 8485

This theorem is used by:  df2o2  8493  2oex  8496  nlim2  8506  ord2eln012  8513  2oconcl  8519  enpr2d  9084  map2xp  9174  snnen2o  9244  rex2dom  9252  1sdom2dom  9253  cantnflem2  9698  xp2dju  10262  sdom2en01  10387  sadcf  16632  fnpr2o  17738  fnpr2ob  17739  fvprif  17742  xpsfrnel  17743  xpsfeq  17744  xpsle  17760  setcepi  18272  setc2obas  18278  setc2ohom  18279  efgi0  19943  efgi1  19944  vrgpf  19991  vrgpinv  19992  frgpuptinv  19994  frgpup2  19999  frgpup3lem  20000  frgpnabllem1  20096  dmdprdpr  20274  dprdpr  20275  xpstopnlem1  24137  xpstopnlem2  24139  xpsxmetlem  24707  xpsdsval  24709  xpsmet  24710  bdaypw2n0bndlem  28858  onint1  37361  pw2f1ocnv  44181  wepwsolem  44186  omnord1ex  44443  oege2  44446  df3o2  44452  oenord1ex  44454  oenord1  44455  oaomoencom  44456  oenassex  44457  omabs2  44471  omcl3g  44473  clsk1independent  45183  setc1onsubc  50876  parswapprop  50913  par2hom  50915  par2diag  50916  fuconuniqlem  50917  fuconuniqvalslem  50919