MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df2o3 Structured version   Visualization version   Unicode version

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
StepHypRef Expression
1 df-2o 7201 . 2  |-  2o  =  suc  1o
2 df-suc 5436 . 2  |-  suc  1o  =  ( 1o  u.  { 1o } )
3 df1o2 7212 . . . 4  |-  1o  =  { (/) }
43uneq1i 3575 . . 3  |-  ( 1o  u.  { 1o }
)  =  ( {
(/) }  u.  { 1o } )
5 df-pr 3962 . . 3  |-  { (/) ,  1o }  =  ( { (/) }  u.  { 1o } )
64, 5eqtr4i 2496 . 2  |-  ( 1o  u.  { 1o }
)  =  { (/) ,  1o }
71, 2, 63eqtri 2497 1  |-  2o  =  { (/) ,  1o }
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator