Theorem limelon 6428

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 6424	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6370	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
3	1, 2	imbitrrid 249	. 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On))
4	3	imp 412	1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  Ord word 6361  Oncon0 6362  Lim wlim 6363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3896  df-uni 4867  df-tr 5212  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366  df-lim 6367

This theorem is used by:  onzsl  7858  limuni3  7864  tfindsg2  7874  dfom2  7880  rdglim  8438  oalim  8544  omlim  8545  oelim  8546  oalimcl  8572  oaass  8573  omlimcl  8590  odi  8591  omass  8592  oen0  8599  oewordri  8605  oelim2  8608  oelimcl  8613  omabs  8664  r1lim  9783  alephordi  10157  cflm  10331  alephsing  10358  pwcfsdom  10672  winafp  10786  r1limwun  10825  omlimcl2  44338  oeord2lim  44405