Theorem 2on 8536

Description: Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) Avoid ax-un 7770. (Revised by BTernaryTau, 30-Nov-2024.)

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8523	. 2 ⊢ 2o = suc 1o
2		1on 8534	. . 3 ⊢ 1o ∈ On
3		2oex 8533	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2841	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7845	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 691	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2840	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2108  Vcvv 3488  Oncon0 6395  suc csuc 6397  1_oc1o 8515  2_oc2o 8516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399  df-suc 6401  df-1o 8522  df-2o 8523

This theorem is referenced by:  ord3  8539  3on  8540  ord2eln012  8553  o2p2e4  8597  oneo  8637  2onn  8698  nneob  8712  en3  9344  infxpenc  10087  infxpenc2  10091  mappwen  10181  pwdjuen  10251  ackbij1lem5  10292  sdom2en01  10371  fin1a2lem4  10472  fin1a2lem6  10474  xpsrnbas  17631  xpsadd  17634  xpsmul  17635  xpsvsca  17637  xpsle  17639  cat1  18164  xpsmnd  18812  xpsgrp  19099  efgval  19759  efgtf  19764  frgpcpbl  19801  frgp0  19802  frgpeccl  19803  frgpadd  19805  frgpmhm  19807  vrgpf  19810  vrgpinv  19811  frgpupf  19815  frgpup1  19817  frgpup2  19818  frgpup3lem  19819  frgpnabllem1  19915  frgpnabllem2  19916  xpsrngd  20206  xpsringd  20355  xpstopnlem1  23838  xpstps  23839  xpstopnlem2  23840  xpsxmetlem  24410  xpsdsval  24412  nofv  27720  sltres  27725  noextendgt  27733  nolesgn2ores  27735  nosepnelem  27742  nosepdmlem  27746  nolt02o  27758  nogt01o  27759  nosupno  27766  nosupbnd1lem3  27773  nosupbnd1  27777  nosupbnd2lem1  27778  nosupbnd2  27779  ssoninhaus  36414  onint1  36415  1oequni2o  37334  finxpreclem4  37360  pw2f1ocnv  42994  frlmpwfi  43055  omnord1  43267  oege2  43269  oenord1  43278  oaomoencom  43279  oenassex  43280  oenass  43281  omabs2  43294  oaltom  43367  omltoe  43369  2no  43399  nlim3  43406  tr3dom  43490  enrelmap  43959