Theorem df2o3 8522

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 8515	. 2 ⊢ 2o = suc 1o
2		df-suc 6394	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8521	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4166	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4591	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2789	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2790	1 ⊢ 2o = {∅, 1o}

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 4152  ∅c0 4281  {csn 4588  {cpr 4590  suc csuc 6390  1_oc1o 8507  2_oc2o 8508

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050  df-un 4154  df-nul 4282  df-pr 4591  df-suc 6394  df-1o 8514  df-2o 8515

This theorem is used by:  df2o2  8523  2oex  8526  nlim2  8536  ord2eln012  8543  2oconcl  8549  enpr2d  9114  map2xp  9204  snnen2o  9274  rex2dom  9282  1sdom2dom  9283  cantnflem2  9728  xp2dju  10294  sdom2en01  10419  sadcf  16667  fnpr2o  17779  fnpr2ob  17780  fvprif  17783  xpsfrnel  17784  xpsfeq  17785  xpsle  17801  setcepi  18313  setc2obas  18319  setc2ohom  18320  efgi0  19985  efgi1  19986  vrgpf  20033  vrgpinv  20034  frgpuptinv  20036  frgpup2  20041  frgpup3lem  20042  frgpnabllem1  20138  dmdprdpr  20316  dprdpr  20317  xpstopnlem1  24183  xpstopnlem2  24185  xpsxmetlem  24753  xpsdsval  24755  xpsmet  24756  bdaypw2n0bndlem  28906  onint1  37452  pw2f1ocnv  44310  wepwsolem  44315  omnord1ex  44567  oege2  44570  df3o2  44576  oenord1ex  44578  oenord1  44579  oaomoencom  44580  oenassex  44581  omabs2  44595  omcl3g  44597  clsk1independent  45307  setc1onsubc  51071  parswapprop  51108  par2hom  51110  par2diag  51111  fuconuniqlem  51112  fuconuniqvalslem  51114