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 6370	. . 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 2144  Ord word 6361  Oncon0 6362  Lim wlim 6363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3896  df-uni 4867  df-tr 5212  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366  df-lim 6367

This theorem is used by:  onzsl  7857  limuni3  7863  tfindsg2  7873  dfom2  7879  rdglim  8434  oalim  8540  omlim  8541  oelim  8542  oalimcl  8568  oaass  8569  omlimcl  8586  odi  8587  omass  8588  oen0  8595  oewordri  8601  oelim2  8604  oelimcl  8609  omabs  8660  r1lim  9779  alephordi  10153  cflm  10327  alephsing  10354  pwcfsdom  10668  winafp  10782  r1limwun  10821  omlimcl2  44244  oeord2lim  44311