Theorem eloni 2958

Description: An ordinal number has the ordinal property.

Assertion

Ref	Expression
eloni	|- (A e. On -> Ord A)

Proof of Theorem eloni

Step	Hyp	Ref	Expression
1		elong 2956	. 2 |- (A e. On -> (A e. On <-> Ord A))
2	1	ibi 592	1 |- (A e. On -> Ord A)

Syntax hints:   -> wi 3   e. wcel 958  Ord word 2947  Oncon0 2948

This theorem is referenced by:  elon2 2959  onelon 2972  onin 2978  ontri1 2981  ordon 2987  ordeleqon 2990  onsst 2992  ssorduni 2993  onelpsst 2998  onsseleq 2999  onelsst 3000  ontr1 3003  ontr2 3004  ordunidif 3005  on0eln0 3024  ordsssuc 3057  onsssuc 3058  onnbtwn 3064  ordsuc 3065  onpwsuc 3067  onsucmin 3072  ordunisuc 3089  onsucuni2 3091  suc11 3093  onord 3095  onssneli 3101  onuninsuc 3108  ordunisuc2 3115  ordzsl 3116  nlimon 3122  nnord 3140  tfinds 3161  tfindsg2 3163  tz7.48lem 3955  oe0m1 4160  oesuc 4166  oaordi 4180  oaord 4181  oacan 4182  oawordri 4184  oalimcl 4194  oaass 4195  omord2 4198  omcan 4200  omwordi 4202  omword1 4204  omword2 4205  om00 4206  omlimcl 4209  omass 4211  oen0 4213  oeord 4215  oecan 4216  oewordi 4218  oeworde 4220  nnarcl 4232  oaabs 4252  omsmo 4257  onomeneq 4519  infensuc 4638  r1ord 4655  r1val1 4658  rankr1 4674  rankval3 4681  bndrank 4682  r1pw 4686  rankbnd2 4704  weth 4787  zorn2lem6 4793  cardnn 4824  ondomcard 4857  carduni 4858  cardaleph 4885  iscard3 4888  alephfp 4900

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 777  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1649  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-tr 2681  df-po 2840  df-so 2850  df-fr 2917  df-we 2934  df-ord 2951  df-on 2952

Copyright terms: Public domain