Theorem limelon 6371

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 6367	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6314	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
3	1, 2	imbitrrid 246	. 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On))
4	3	imp 406	1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  Ord word 6305  Oncon0 6306  Lim wlim 6307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-v 3438  df-ss 3919  df-uni 4860  df-tr 5199  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-ord 6309  df-on 6310  df-lim 6311

This theorem is referenced by:  onzsl  7776  limuni3  7782  tfindsg2  7792  dfom2  7798  rdglim  8345  oalim  8447  omlim  8448  oelim  8449  oalimcl  8475  oaass  8476  omlimcl  8493  odi  8494  omass  8495  oen0  8501  oewordri  8507  oelim2  8510  oelimcl  8515  omabs  8566  r1lim  9665  alephordi  9965  cflm  10141  alephsing  10167  pwcfsdom  10474  winafp  10588  r1limwun  10627  omlimcl2  43281  oeord2lim  43348