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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  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 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-v 3465  df-ss 3930  df-uni 4874  df-tr 5220  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6360  df-on 6361  df-lim 6362

This theorem is referenced by:  onzsl  7838  limuni3  7844  tfindsg2  7854  dfom2  7860  rdglim  8409  oalim  8513  omlim  8514  oelim  8515  oalimcl  8541  oaass  8542  omlimcl  8559  odi  8560  omass  8561  oen0  8568  oewordri  8574  oelim2  8577  oelimcl  8582  omabs  8633  r1lim  9740  alephordi  10054  cflm  10229  alephsing  10256  pwcfsdom  10564  winafp  10678  r1limwun  10717  omlimcl2  43854  oeord2lim  43921