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

Theorem 2on 8102
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 8094 . 2 2o = suc 1o
2 1on 8100 . . 3 1o ∈ On
32onsuci 7541 . 2 suc 1o ∈ On
41, 3eqeltri 2909 1 2o ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Oncon0 6185  suc csuc 6187  1oc1o 8086  2oc2o 8087
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-tr 5165  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-ord 6188  df-on 6189  df-suc 6191  df-1o 8093  df-2o 8094
This theorem is referenced by:  3on  8105  o2p2e4  8157  oneo  8197  nneob  8269  infxpenc  9433  infxpenc2  9437  mappwen  9527  pwdjuen  9596  ackbij1lem5  9635  sdom2en01  9713  fin1a2lem4  9814  fin1a2lem6  9816  xpsrnbas  16834  xpsadd  16837  xpsmul  16838  xpsvsca  16840  xpsle  16842  xpsmnd  17941  xpsgrp  18158  efgval  18774  efgtf  18779  frgpcpbl  18816  frgp0  18817  frgpeccl  18818  frgpadd  18820  frgpmhm  18822  vrgpf  18825  vrgpinv  18826  frgpupf  18830  frgpup1  18832  frgpup2  18833  frgpup3lem  18834  frgpnabllem1  18924  frgpnabllem2  18925  xpstopnlem1  22347  xpstps  22348  xpstopnlem2  22349  xpsxmetlem  22918  xpsdsval  22920  nofv  33062  sltres  33067  noextendgt  33075  nolesgn2ores  33077  nosepnelem  33082  nosepdmlem  33085  nolt02o  33097  nosupno  33101  nosupbday  33103  nosupbnd1lem3  33108  nosupbnd1  33112  nosupbnd2lem1  33113  nosupbnd2  33114  ssoninhaus  33694  onint1  33695  1oequni2o  34532  finxpreclem4  34558  pw2f1ocnv  39514  frlmpwfi  39578  tr3dom  39774  enrelmap  40223
  Copyright terms: Public domain W3C validator