MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2on Unicode version

Theorem 2on 6889
Description: Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
Assertion
Ref Expression
2on

Proof of Theorem 2on
StepHypRef Expression
1 df-2o 6882 . 2
2 1on 6888 . . 3
32onsuci 6419 . 2
41, 3eqeltri 2492 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1749   con0 4690  succsuc 4692   c1o 6874   c2o 6875
This theorem is referenced by:  3on  6891  oneo  6981  infxpenc  8131  infxpenc2  8135  infxpencOLD  8136  infxpenc2OLD  8139  mappwen  8229  pwcdaen  8301  sdom2en01  8418  fin1a2lem4  8519  xpslem  14451  xpsadd  14454  xpsmul  14455  xpsvsca  14457  xpsle  14459  xpsmnd  15401  xpsgrp  15611  efgval  16151  efgtf  16156  frgpcpbl  16193  frgp0  16194  frgpeccl  16195  frgpadd  16197  frgpmhm  16199  vrgpf  16202  vrgpinv  16203  frgpupf  16207  frgpup1  16209  frgpup2  16210  frgpup3lem  16211  frgpnabllem1  16287  frgpnabllem2  16288  xpstopnlem1  19086  xpstps  19087  xpstopnlem2  19088  xpsxmetlem  19654  xpsdsval  19656  nofv  27500  sltres  27507  noxp2o  27510  nobndup  27543  ssoninhaus  27997  onint1  27998  pw2f1ocnv  29059  frlmpwfi  29126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pr 4503  ax-un 6342
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3or 951  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-ral 2699  df-rex 2700  df-rab 2703  df-v 2953  df-sbc 3165  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-pss 3321  df-nul 3615  df-if 3769  df-pw 3839  df-sn 3859  df-pr 3860  df-tp 3861  df-op 3862  df-uni 4067  df-br 4268  df-opab 4326  df-tr 4361  df-eprel 4603  df-po 4612  df-so 4613  df-fr 4650  df-we 4652  df-ord 4693  df-on 4694  df-suc 4696  df-1o 6881  df-2o 6882
  Copyright terms: Public domain W3C validator