Theorem limelon 6397

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 6393	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6340	. . 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 6331  Oncon0 6332  Lim wlim 6333

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 3449  df-ss 3931  df-uni 4872  df-tr 5215  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336  df-lim 6337

This theorem is referenced by:  onzsl  7822  limuni3  7828  tfindsg2  7838  dfom2  7844  rdglim  8394  oalim  8496  omlim  8497  oelim  8498  oalimcl  8524  oaass  8525  omlimcl  8542  odi  8543  omass  8544  oen0  8550  oewordri  8556  oelim2  8559  oelimcl  8564  omabs  8615  r1lim  9725  alephordi  10027  cflm  10203  alephsing  10229  pwcfsdom  10536  winafp  10650  r1limwun  10689  omlimcl2  43231  oeord2lim  43298