Theorem limelon 6376

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 6372	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6319	. . 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 6310  Oncon0 6311  Lim wlim 6312

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3440  df-ss 3922  df-uni 4862  df-tr 5203  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-ord 6314  df-on 6315  df-lim 6316

This theorem is referenced by:  onzsl  7786  limuni3  7792  tfindsg2  7802  dfom2  7808  rdglim  8355  oalim  8457  omlim  8458  oelim  8459  oalimcl  8485  oaass  8486  omlimcl  8503  odi  8504  omass  8505  oen0  8511  oewordri  8517  oelim2  8520  oelimcl  8525  omabs  8576  r1lim  9687  alephordi  9987  cflm  10163  alephsing  10189  pwcfsdom  10496  winafp  10610  r1limwun  10649  omlimcl2  43218  oeord2lim  43285