Theorem limelon 6423

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3916  df-uni 4868  df-tr 5213  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6360  df-on 6361  df-lim 6362

This theorem is used by:  onzsl  7842  limuni3  7848  tfindsg2  7858  dfom2  7864  rdglim  8415  oalim  8519  omlim  8520  oelim  8521  oalimcl  8547  oaass  8548  omlimcl  8565  odi  8566  omass  8567  oen0  8574  oewordri  8580  oelim2  8583  oelimcl  8588  omabs  8639  r1lim  9754  alephordi  10077  cflm  10251  alephsing  10278  pwcfsdom  10592  winafp  10706  r1limwun  10745  omlimcl2  44083  oeord2lim  44150