Theorem limelon 6422

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 6418	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6365	. . 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 2109  Ord word 6356  Oncon0 6357  Lim wlim 6358

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 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-v 3466  df-ss 3948  df-uni 4889  df-tr 5235  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6360  df-on 6361  df-lim 6362

This theorem is referenced by:  onzsl  7846  limuni3  7852  tfindsg2  7862  dfom2  7868  rdglim  8445  oalim  8549  omlim  8550  oelim  8551  oalimcl  8577  oaass  8578  omlimcl  8595  odi  8596  omass  8597  oen0  8603  oewordri  8609  oelim2  8612  oelimcl  8617  omabs  8668  r1lim  9791  alephordi  10093  cflm  10269  alephsing  10295  pwcfsdom  10602  winafp  10716  r1limwun  10755  omlimcl2  43233  oeord2lim  43300