Theorem limelon 5505

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 5501	. . 3 |- ( Lim A -> Ord A )
2		elong 5450	. . 3 |- ( A e. B -> ( A e. On <-> Ord A ) )
3	1, 2	syl5ibr 229	. 2 |- ( A e. B -> ( Lim A -> A e. On ) )
4	3	imp 435	1 |- ( ( A e. B /\ Lim A ) -> A e. On )

Syntax hints:   -> wi 4   /\ wa 375   e. wcel 1898   Ord word 5441   Oncon0 5442   Lim wlim 5443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rex 2755  df-v 3059  df-in 3423  df-ss 3430  df-uni 4213  df-tr 4512  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-ord 5445  df-on 5446  df-lim 5447

This theorem is referenced by:  onzsl  6700  limuni3  6706  tfindsg2  6715  dfom2  6721  rdglim  7170  oalim  7260  omlim  7261  oelim  7262  oalimcl  7287  oaass  7288  omlimcl  7305  odi  7306  omass  7307  oen0  7313  oewordri  7319  oelim2  7322  oelimcl  7327  omabs  7374  r1lim  8269  alephordi  8531  cflm  8706  alephsing  8732  pwcfsdom  9034  winafp  9148  r1limwun  9187