Theorem 2on 8450

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8438	. 2 ⊢ 2o = suc 1o
2		1on 8449	. . 3 ⊢ 1o ∈ On
3		2oex 8448	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2826	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7788	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2825	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2109  Vcvv 3450  Oncon0 6335  suc csuc 6337  1_oc1o 8430  2_oc2o 8431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339  df-suc 6341  df-1o 8437  df-2o 8438

This theorem is referenced by:  ord3  8452  3on  8453  ord2eln012  8464  o2p2e4  8508  oneo  8548  2onn  8609  nneob  8623  en3  9234  infxpenc  9978  infxpenc2  9982  mappwen  10072  pwdjuen  10142  ackbij1lem5  10183  sdom2en01  10262  fin1a2lem4  10363  fin1a2lem6  10365  xpsrnbas  17541  xpsadd  17544  xpsmul  17545  xpsvsca  17547  xpsle  17549  cat1  18066  xpsmnd  18711  xpsgrp  18998  efgval  19654  efgtf  19659  frgpcpbl  19696  frgp0  19697  frgpeccl  19698  frgpadd  19700  frgpmhm  19702  vrgpf  19705  vrgpinv  19706  frgpupf  19710  frgpup1  19712  frgpup2  19713  frgpup3lem  19714  frgpnabllem1  19810  frgpnabllem2  19811  xpsrngd  20095  xpsringd  20248  xpstopnlem1  23703  xpstps  23704  xpstopnlem2  23705  xpsxmetlem  24274  xpsdsval  24276  nofv  27576  sltres  27581  noextendgt  27589  nolesgn2ores  27591  nosepnelem  27598  nosepdmlem  27602  nolt02o  27614  nogt01o  27615  nosupno  27622  nosupbnd1lem3  27629  nosupbnd1  27633  nosupbnd2lem1  27634  nosupbnd2  27635  ssoninhaus  36443  onint1  36444  1oequni2o  37363  finxpreclem4  37389  pw2f1ocnv  43033  frlmpwfi  43094  omnord1  43301  oege2  43303  oenord1  43312  oaomoencom  43313  oenassex  43314  oenass  43315  omabs2  43328  oaltom  43401  omltoe  43403  2no  43433  nlim3  43440  tr3dom  43524  enrelmap  43993  nelsubc3  49064