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

Theorem 2on 7516
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 2𝑜 ∈ On

Proof of Theorem 2on
StepHypRef Expression
1 df-2o 7509 . 2 2𝑜 = suc 1𝑜
2 1on 7515 . . 3 1𝑜 ∈ On
32onsuci 6988 . 2 suc 1𝑜 ∈ On
41, 3eqeltri 2694 1 2𝑜 ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  Oncon0 5684  suc csuc 5686  1𝑜c1o 7501  2𝑜c2o 7502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pr 4869  ax-un 6905
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3419  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-br 4616  df-opab 4676  df-tr 4715  df-eprel 4987  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-ord 5687  df-on 5688  df-suc 5690  df-1o 7508  df-2o 7509
This theorem is referenced by:  3on  7518  o2p2e4  7569  oneo  7609  infxpenc  8788  infxpenc2  8792  mappwen  8882  pwcdaen  8954  sdom2en01  9071  fin1a2lem4  9172  xpslem  16157  xpsadd  16160  xpsmul  16161  xpsvsca  16163  xpsle  16165  xpsmnd  17254  xpsgrp  17458  efgval  18054  efgtf  18059  frgpcpbl  18096  frgp0  18097  frgpeccl  18098  frgpadd  18100  frgpmhm  18102  vrgpf  18105  vrgpinv  18106  frgpupf  18110  frgpup1  18112  frgpup2  18113  frgpup3lem  18114  frgpnabllem1  18200  frgpnabllem2  18201  xpstopnlem1  21525  xpstps  21526  xpstopnlem2  21527  xpsxmetlem  22097  xpsdsval  22099  nofv  31532  sltres  31539  noxp2o  31542  noextendgt  31548  nobndup  31584  nosepnelem  31586  nosepdmlem  31588  nosino  31596  ssoninhaus  32110  onint1  32111  1oequni2o  32869  finxpreclem4  32884  pw2f1ocnv  37105  frlmpwfi  37169  enrelmap  37794  clsk1indlem1  37846  clsk1independent  37847
  Copyright terms: Public domain W3C validator