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

Theorem 2on 8089
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 2o ∈ On

Proof of Theorem 2on
StepHypRef Expression
1 df-2o 8081 . 2 2o = suc 1o
2 1on 8087 . . 3 1o ∈ On
32onsuci 7531 . 2 suc 1o ∈ On
41, 3eqeltri 2907 1 2o ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  Oncon0 6167  suc csuc 6169  1oc1o 8073  2oc2o 8074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pr 5306  ax-un 7439
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-sbc 3753  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-br 5043  df-opab 5105  df-tr 5149  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-we 5492  df-ord 6170  df-on 6171  df-suc 6173  df-1o 8080  df-2o 8081
This theorem is referenced by:  3on  8092  o2p2e4  8144  o2p2e4OLD  8145  oneo  8185  nneob  8257  infxpenc  9422  infxpenc2  9426  mappwen  9516  pwdjuen  9585  ackbij1lem5  9624  sdom2en01  9702  fin1a2lem4  9803  fin1a2lem6  9805  xpsrnbas  16823  xpsadd  16826  xpsmul  16827  xpsvsca  16829  xpsle  16831  xpsmnd  17930  xpsgrp  18197  efgval  18822  efgtf  18827  frgpcpbl  18864  frgp0  18865  frgpeccl  18866  frgpadd  18868  frgpmhm  18870  vrgpf  18873  vrgpinv  18874  frgpupf  18878  frgpup1  18880  frgpup2  18881  frgpup3lem  18882  frgpnabllem1  18972  frgpnabllem2  18973  xpstopnlem1  22393  xpstps  22394  xpstopnlem2  22395  xpsxmetlem  22965  xpsdsval  22967  nofv  33172  sltres  33177  noextendgt  33185  nolesgn2ores  33187  nosepnelem  33192  nosepdmlem  33195  nolt02o  33207  nosupno  33211  nosupbday  33213  nosupbnd1lem3  33218  nosupbnd1  33222  nosupbnd2lem1  33223  nosupbnd2  33224  ssoninhaus  33804  onint1  33805  1oequni2o  34666  finxpreclem4  34692  pw2f1ocnv  39771  frlmpwfi  39835  tr3dom  40029  enrelmap  40478
  Copyright terms: Public domain W3C validator