Theorem limelon 6459

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 6455	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6403	. . 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 2108  Ord word 6394  Oncon0 6395  Lim wlim 6396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-v 3490  df-ss 3993  df-uni 4932  df-tr 5284  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399  df-lim 6400

This theorem is referenced by:  onzsl  7883  limuni3  7889  tfindsg2  7899  dfom2  7905  rdglim  8482  oalim  8588  omlim  8589  oelim  8590  oalimcl  8616  oaass  8617  omlimcl  8634  odi  8635  omass  8636  oen0  8642  oewordri  8648  oelim2  8651  oelimcl  8656  omabs  8707  r1lim  9841  alephordi  10143  cflm  10319  alephsing  10345  pwcfsdom  10652  winafp  10766  r1limwun  10805  omlimcl2  43203  oeord2lim  43271