Theorem limelon 6314

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 6310	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6259	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
3	1, 2	syl5ibr 245	. 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On))
4	3	imp 406	1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Ord word 6250  Oncon0 6251  Lim wlim 6252

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-tr 5188  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-ord 6254  df-on 6255  df-lim 6256

This theorem is referenced by:  onzsl  7668  limuni3  7674  tfindsg2  7683  dfom2  7689  rdglim  8228  oalim  8324  omlim  8325  oelim  8326  oalimcl  8353  oaass  8354  omlimcl  8371  odi  8372  omass  8373  oen0  8379  oewordri  8385  oelim2  8388  oelimcl  8393  omabs  8441  r1lim  9461  alephordi  9761  cflm  9937  alephsing  9963  pwcfsdom  10270  winafp  10384  r1limwun  10423