Theorem 1on 8108

Description: Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.)

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8101	. 2 ⊢ 1o = suc ∅
2		0elon 6243	. . 3 ⊢ ∅ ∈ On
3	2	onsuci 7552	. 2 ⊢ suc ∅ ∈ On
4	1, 3	eqeltri 2909	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2110  ∅c0 4290  Oncon0 6190  suc csuc 6192  1_oc1o 8094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329  ax-un 7460

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  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 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-tr 5172  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-ord 6193  df-on 6194  df-suc 6196  df-1o 8101

This theorem is referenced by:  1oex  8109  2on  8110  ondif2  8126  2oconcl  8127  fnoe  8134  oesuclem  8149  oecl  8161  o1p1e2  8164  o2p2e4OLD  8166  om1r  8168  oe1m  8170  omword1  8198  omword2  8199  omlimcl  8203  oneo  8206  oewordi  8216  oelim2  8220  oeoa  8222  oeoe  8224  oeeui  8227  oaabs2  8271  enpr2d  8596  sucxpdom  8726  oancom  9113  cnfcom3lem  9165  pm54.43lem  9427  pm54.43  9428  infxpenc  9443  infxpenc2  9447  undjudom  9592  endjudisj  9593  djuen  9594  dju1p1e2  9598  dju1p1e2ALT  9599  xpdjuen  9604  mapdjuen  9605  djuxpdom  9610  djufi  9611  djuinf  9613  infdju1  9614  pwdju1  9615  pwdjudom  9637  isfin4p1  9736  pwxpndom2  10086  wunex2  10159  wuncval2  10168  tsk2  10186  efgmnvl  18839  frgpnabllem1  18992  dmdprdpr  19170  dprdpr  19171  psr1crng  20354  psr1assa  20355  psr1tos  20356  psr1bas  20358  vr1cl2  20360  ply1lss  20363  ply1subrg  20364  ressply1bas2  20395  ressply1add  20397  ressply1mul  20398  ressply1vsca  20399  subrgply1  20400  ply1plusgfvi  20409  psr1ring  20414  psr1lmod  20416  psr1sca  20417  ply1ascl  20425  subrg1ascl  20426  subrg1asclcl  20427  subrgvr1  20428  subrgvr1cl  20429  coe1z  20430  coe1mul2lem1  20434  coe1mul2  20436  coe1tm  20440  evls1val  20482  evls1rhm  20484  evls1sca  20485  evl1val  20491  evl1rhm  20494  evl1sca  20496  evl1var  20498  evls1var  20500  mpfpf1  20513  pf1mpf  20514  pf1ind  20517  xkofvcn  22291  xpstopnlem1  22416  ufildom1  22533  deg1z  24680  deg1addle  24694  deg1vscale  24697  deg1vsca  24698  deg1mulle2  24702  deg1le0  24704  ply1nzb  24715  sltval2  33163  noextendlt  33176  sltsolem1  33180  nosepnelem  33184  nolt02o  33199  rankeq1o  33632  ssoninhaus  33796  onint1  33797  1oequni2o  34648  finxp1o  34672  finxpreclem3  34673  finxpreclem4  34674  finxpreclem5  34675  finxpsuclem  34677  pw2f1ocnv  39632  wepwsolem  39640  pwfi2f1o  39694  sn1dom  39890  pr2dom  39891  tr3dom  39892  clsk1indlem4  40392  ply1ass23l  44435