Theorem limelon 4941

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 4937	. . 3 |- ( Lim A -> Ord A )
2		elong 4886	. . 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 1767   Ord word 4877   Oncon0 4878   Lim wlim 4879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-v 3115  df-in 3483  df-ss 3490  df-uni 4246  df-tr 4541  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883

This theorem is referenced by:  onzsl  6659  limuni3  6665  tfindsg2  6674  dfom2  6680  rdglim  7089  oalim  7179  omlim  7180  oelim  7181  oalimcl  7206  oaass  7207  omlimcl  7224  odi  7225  omass  7226  oen0  7232  oewordri  7238  oelim2  7241  oelimcl  7246  omabs  7293  r1lim  8186  alephordi  8451  cflm  8626  alephsing  8652  pwcfsdom  8954  winafp  9071  r1limwun  9110