Theorem limord 6325

Description: A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)

Assertion

Ref	Expression
limord	⊢ (Lim 𝐴 → Ord 𝐴)

Proof of Theorem limord

Step	Hyp	Ref	Expression
1		df-lim 6271	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
2	1	simp1bi 1144	1 ⊢ (Lim 𝐴 → Ord 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2943  ∅c0 4256  ∪ cuni 4839  Ord word 6265  Lim wlim 6267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-lim 6271

This theorem is referenced by:  0ellim  6328  limelon  6329  nlimsucg  7689  ordzsl  7692  limsuc  7696  limsssuc  7697  limomss  7717  trom  7721  limom  7728  tfr2b  8227  rdgsucg  8254  rdglimg  8256  rdglim2  8263  1ellim  8328  2ellim  8329  oesuclem  8355  odi  8410  omeulem1  8413  oelim2  8426  oeoalem  8427  oeoelem  8429  limenpsi  8939  limensuci  8940  ordtypelem3  9279  ordtypelem5  9281  ordtypelem6  9282  ordtypelem7  9283  ordtypelem9  9285  r1tr  9534  r1ordg  9536  r1ord3g  9537  r1pwss  9542  r1val1  9544  rankwflemb  9551  r1elwf  9554  rankr1ai  9556  rankr1ag  9560  rankr1bg  9561  unwf  9568  rankr1clem  9578  rankr1c  9579  rankval3b  9584  rankonidlem  9586  onssr1  9589  coflim  10017  cflim3  10018  cflim2  10019  cfss  10021  cfslb  10022  cfslbn  10023  cfslb2n  10024  r1limwun  10492  inar1  10531  rdgprc  33770  oldlim  34069  limsucncmpi  34634  grur1cld  41850