Theorem limelon 6400

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 6396	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6343	. . 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 2109  Ord word 6334  Oncon0 6335  Lim wlim 6336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3452  df-ss 3934  df-uni 4875  df-tr 5218  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339  df-lim 6340

This theorem is referenced by:  onzsl  7825  limuni3  7831  tfindsg2  7841  dfom2  7847  rdglim  8397  oalim  8499  omlim  8500  oelim  8501  oalimcl  8527  oaass  8528  omlimcl  8545  odi  8546  omass  8547  oen0  8553  oewordri  8559  oelim2  8562  oelimcl  8567  omabs  8618  r1lim  9732  alephordi  10034  cflm  10210  alephsing  10236  pwcfsdom  10543  winafp  10657  r1limwun  10696  omlimcl2  43238  oeord2lim  43305