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

Theorem 2on 7722
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 7714 . 2 2𝑜 = suc 1𝑜
2 1on 7720 . . 3 1𝑜 ∈ On
32onsuci 7185 . 2 suc 1𝑜 ∈ On
41, 3eqeltri 2846 1 2𝑜 ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 2145  Oncon0 5866  suc csuc 5868  1𝑜c1o 7706  2𝑜c2o 7707
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-tr 4887  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-ord 5869  df-on 5870  df-suc 5872  df-1o 7713  df-2o 7714
This theorem is referenced by:  3on  7724  o2p2e4  7775  oneo  7815  infxpenc  9041  infxpenc2  9045  mappwen  9135  pwcdaen  9209  ackbij1lem5  9248  sdom2en01  9326  fin1a2lem4  9427  xpslem  16441  xpsadd  16444  xpsmul  16445  xpsvsca  16447  xpsle  16449  xpsmnd  17538  xpsgrp  17742  efgval  18337  efgtf  18342  frgpcpbl  18379  frgp0  18380  frgpeccl  18381  frgpadd  18383  frgpmhm  18385  vrgpf  18388  vrgpinv  18389  frgpupf  18393  frgpup1  18395  frgpup2  18396  frgpup3lem  18397  frgpnabllem1  18483  frgpnabllem2  18484  xpstopnlem1  21833  xpstps  21834  xpstopnlem2  21835  xpsxmetlem  22404  xpsdsval  22406  nofv  32147  sltres  32152  noextendgt  32160  nolesgn2ores  32162  nosepnelem  32167  nosepdmlem  32170  nolt02o  32182  nosupno  32186  nosupbday  32188  nosupbnd1lem3  32193  nosupbnd1  32197  nosupbnd2lem1  32198  nosupbnd2  32199  ssoninhaus  32784  onint1  32785  1oequni2o  33553  finxpreclem4  33568  pw2f1ocnv  38130  frlmpwfi  38194  enrelmap  38817  clsk1indlem1  38869  clsk1independent  38870
  Copyright terms: Public domain W3C validator