Theorem limelon 6329

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

Assertion

Ref	Expression
limelon	⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

Proof of Theorem limelon

Step	Hyp	Ref	Expression
1		limord 6325	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6274	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
3	1, 2	syl5ibr 245	. 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On))
4	3	imp 407	1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Ord word 6265  Oncon0 6266  Lim wlim 6267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-tr 5192  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-ord 6269  df-on 6270  df-lim 6271

This theorem is referenced by:  onzsl  7693  limuni3  7699  tfindsg2  7708  dfom2  7714  rdglim  8257  oalim  8362  omlim  8363  oelim  8364  oalimcl  8391  oaass  8392  omlimcl  8409  odi  8410  omass  8411  oen0  8417  oewordri  8423  oelim2  8426  oelimcl  8431  omabs  8481  r1lim  9530  alephordi  9830  cflm  10006  alephsing  10032  pwcfsdom  10339  winafp  10453  r1limwun  10492