Theorem limelon 4782

Description: A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.)

Assertion

Ref	Expression
limelon	|- ( ( A e. B /\ Lim A ) -> A e. On )

Proof of Theorem limelon

Step	Hyp	Ref	Expression
1		limord 4778	. . 3 |- ( Lim A -> Ord A )
2		elong 4727	. . 3 |- ( A e. B -> ( A e. On <-> Ord A ) )
3	1, 2	syl5ibr 221	. 2 |- ( A e. B -> ( Lim A -> A e. On ) )
4	3	imp 429	1 |- ( ( A e. B /\ Lim A ) -> A e. On )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1756   Ord word 4718   Oncon0 4719   Lim wlim 4720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720  df-rex 2721  df-v 2974  df-in 3335  df-ss 3342  df-uni 4092  df-tr 4386  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724

This theorem is referenced by:  onzsl  6457  limuni3  6463  tfindsg2  6472  dfom2  6478  rdglim  6882  oalim  6972  omlim  6973  oelim  6974  oalimcl  6999  oaass  7000  omlimcl  7017  odi  7018  omass  7019  oen0  7025  oewordri  7031  oelim2  7034  oelimcl  7039  omabs  7086  r1lim  7979  alephordi  8244  cflm  8419  alephsing  8445  pwcfsdom  8747  winafp  8864  r1limwun  8903