Theorem limelon 6276

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 6272	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6221	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
3	1, 2	syl5ibr 249	. 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On))
4	3	imp 410	1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2110  Ord word 6212  Oncon0 6213  Lim wlim 6214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-v 3410  df-in 3873  df-ss 3883  df-uni 4820  df-tr 5162  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-ord 6216  df-on 6217  df-lim 6218

This theorem is referenced by:  onzsl  7625  limuni3  7631  tfindsg2  7640  dfom2  7646  rdglim  8162  oalim  8259  omlim  8260  oelim  8261  oalimcl  8288  oaass  8289  omlimcl  8306  odi  8307  omass  8308  oen0  8314  oewordri  8320  oelim2  8323  oelimcl  8328  omabs  8376  r1lim  9388  alephordi  9688  cflm  9864  alephsing  9890  pwcfsdom  10197  winafp  10311  r1limwun  10350