Theorem df2o3 7200

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 7188	. 2 |- 2o = suc 1o
2		df-suc 5445	. 2 |- suc 1o = ( 1o u. { 1o } )
3		df1o2 7199	. . . 4 |- 1o = { (/) }
4	3	uneq1i 3616	. . 3 |- ( 1o u. { 1o } ) = ( { (/) } u. { 1o } )
5		df-pr 3999	. . 3 |- { (/) , 1o } = ( { (/) } u. { 1o } )
6	4, 5	eqtr4i 2454	. 2 |- ( 1o u. { 1o } ) = { (/) , 1o }
7	1, 2, 6	3eqtri 2455	1 |- 2o = { (/) , 1o }

Syntax hints:   = wceq 1437   u. cun 3434   (/)c0 3761   {csn 3996   {cpr 3998   suc csuc 5441   1oc1o 7180   2oc2o 7181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-dif 3439  df-un 3441  df-nul 3762  df-pr 3999  df-suc 5445  df-1o 7187  df-2o 7188

This theorem is referenced by:  df2o2  7201  2oconcl  7210  map2xp  7745  1sdom  7778  cantnflem2  8197  xp2cda  8611  sdom2en01  8733  sadcf  14415  xpscfn  15453  xpscfv  15456  xpsfrnel  15457  xpsfeq  15458  xpsfrnel2  15459  xpsle  15475  setcepi  15971  efgi0  17358  efgi1  17359  vrgpf  17406  vrgpinv  17407  frgpuptinv  17409  frgpup2  17414  frgpup3lem  17415  frgpnabllem1  17497  dmdprdpr  17670  dprdpr  17671  xpstopnlem1  20811  xpstopnlem2  20813  xpsxmetlem  21381  xpsdsval  21383  xpsmet  21384  onint1  31102  pw2f1ocnv  35812  wepwsolem  35820