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 411	1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  Ord word 6361  Oncon0 6362  Lim wlim 6363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-v 3457  df-ss 3923  df-uni 4874  df-tr 5220  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6365  df-on 6366  df-lim 6367

This theorem is referenced by:  onzsl  7843  limuni3  7849  tfindsg2  7859  dfom2  7865  rdglim  8414  oalim  8518  omlim  8519  oelim  8520  oalimcl  8546  oaass  8547  omlimcl  8564  odi  8565  omass  8566  oen0  8573  oewordri  8579  oelim2  8582  oelimcl  8587  omabs  8638  r1lim  9745  alephordi  10059  cflm  10234  alephsing  10261  pwcfsdom  10569  winafp  10683  r1limwun  10722  omlimcl2  43952  oeord2lim  44019