Theorem limelon 6448

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 6444	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6392	. . 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 6383  Oncon0 6384  Lim wlim 6385

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-ss 3968  df-uni 4908  df-tr 5260  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-lim 6389

This theorem is referenced by:  onzsl  7867  limuni3  7873  tfindsg2  7883  dfom2  7889  rdglim  8466  oalim  8570  omlim  8571  oelim  8572  oalimcl  8598  oaass  8599  omlimcl  8616  odi  8617  omass  8618  oen0  8624  oewordri  8630  oelim2  8633  oelimcl  8638  omabs  8689  r1lim  9812  alephordi  10114  cflm  10290  alephsing  10316  pwcfsdom  10623  winafp  10737  r1limwun  10776  omlimcl2  43254  oeord2lim  43322