Theorem limelon 6378

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 6374	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6321	. . 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 6312  Oncon0 6313  Lim wlim 6314

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-v 3439  df-ss 3915  df-uni 4861  df-tr 5203  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6316  df-on 6317  df-lim 6318

This theorem is referenced by:  onzsl  7784  limuni3  7790  tfindsg2  7800  dfom2  7806  rdglim  8353  oalim  8455  omlim  8456  oelim  8457  oalimcl  8483  oaass  8484  omlimcl  8501  odi  8502  omass  8503  oen0  8509  oewordri  8515  oelim2  8518  oelimcl  8523  omabs  8574  r1lim  9674  alephordi  9974  cflm  10150  alephsing  10176  pwcfsdom  10483  winafp  10597  r1limwun  10636  omlimcl2  43362  oeord2lim  43429