Theorem limelon 6382

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 6378	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6325	. . 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 2113  Ord word 6316  Oncon0 6317  Lim wlim 6318

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3442  df-ss 3918  df-uni 4864  df-tr 5206  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-lim 6322

This theorem is referenced by:  onzsl  7788  limuni3  7794  tfindsg2  7804  dfom2  7810  rdglim  8357  oalim  8459  omlim  8460  oelim  8461  oalimcl  8487  oaass  8488  omlimcl  8505  odi  8506  omass  8507  oen0  8514  oewordri  8520  oelim2  8523  oelimcl  8528  omabs  8579  r1lim  9684  alephordi  9984  cflm  10160  alephsing  10186  pwcfsdom  10494  winafp  10608  r1limwun  10647  omlimcl2  43484  oeord2lim  43551