Theorem df2o3 7213

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 7201	. 2 |- 2o = suc 1o
2		df-suc 5436	. 2 |- suc 1o = ( 1o u. { 1o } )
3		df1o2 7212	. . . 4 |- 1o = { (/) }
4	3	uneq1i 3575	. . 3 |- ( 1o u. { 1o } ) = ( { (/) } u. { 1o } )
5		df-pr 3962	. . 3 |- { (/) , 1o } = ( { (/) } u. { 1o } )
6	4, 5	eqtr4i 2496	. 2 |- ( 1o u. { 1o } ) = { (/) , 1o }
7	1, 2, 6	3eqtri 2497	1 |- 2o = { (/) , 1o }

Syntax hints:   = wceq 1452   u. cun 3388   (/)c0 3722   {csn 3959   {cpr 3961   suc csuc 5432   1oc1o 7193   2oc2o 7194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-dif 3393  df-un 3395  df-nul 3723  df-pr 3962  df-suc 5436  df-1o 7200  df-2o 7201

This theorem is referenced by:  df2o2  7214  2oconcl  7223  map2xp  7760  1sdom  7793  cantnflem2  8213  xp2cda  8628  sdom2en01  8750  sadcf  14506  xpscfn  15543  xpscfv  15546  xpsfrnel  15547  xpsfeq  15548  xpsfrnel2  15549  xpsle  15565  setcepi  16061  efgi0  17448  efgi1  17449  vrgpf  17496  vrgpinv  17497  frgpuptinv  17499  frgpup2  17504  frgpup3lem  17505  frgpnabllem1  17587  dmdprdpr  17760  dprdpr  17761  xpstopnlem1  20901  xpstopnlem2  20903  xpsxmetlem  21472  xpsdsval  21474  xpsmet  21475  onint1  31180  pw2f1ocnv  35963  wepwsolem  35971