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 6372	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
3	1, 2	imbitrrid 245	. 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On))
4	3	imp 407	1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Ord word 6363  Oncon0 6364  Lim wlim 6365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909  df-tr 5266  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-ord 6367  df-on 6368  df-lim 6369

This theorem is referenced by:  onzsl  7837  limuni3  7843  tfindsg2  7853  dfom2  7859  rdglim  8428  oalim  8534  omlim  8535  oelim  8536  oalimcl  8562  oaass  8563  omlimcl  8580  odi  8581  omass  8582  oen0  8588  oewordri  8594  oelim2  8597  oelimcl  8602  omabs  8652  r1lim  9769  alephordi  10071  cflm  10247  alephsing  10273  pwcfsdom  10580  winafp  10694  r1limwun  10733  omlimcl2  42293  oeord2lim  42361