Theorem df2o3 8133

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 8119	. 2 ⊢ 2o = suc 1o
2		df-suc 6180	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8132	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4066	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4528	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2784	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2785	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1538   ∪ cun 3858  ∅c0 4227  {csn 4525  {cpr 4527  suc csuc 6176  1_oc1o 8111  2_oc2o 8112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-dif 3863  df-un 3865  df-nul 4228  df-pr 4528  df-suc 6180  df-1o 8118  df-2o 8119

This theorem is referenced by:  df2o2  8134  2oconcl  8144  map2xp  8722  1sdom  8772  cantnflem2  9199  xp2dju  9649  sdom2en01  9775  sadcf  15865  fnpr2o  16901  fnpr2ob  16902  fvprif  16905  xpsfrnel  16906  xpsfeq  16907  xpsle  16923  setcepi  17427  efgi0  18926  efgi1  18927  vrgpf  18974  vrgpinv  18975  frgpuptinv  18977  frgpup2  18982  frgpup3lem  18983  frgpnabllem1  19074  dmdprdpr  19252  dprdpr  19253  xpstopnlem1  22522  xpstopnlem2  22524  xpsxmetlem  23094  xpsdsval  23096  xpsmet  23097  onint1  34221  pw2f1ocnv  40386  wepwsolem  40394  df3o2  41135  clsk1independent  41157