Theorem limelon 6390

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 6386	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6333	. . 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 2114  Ord word 6324  Oncon0 6325  Lim wlim 6326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3444  df-ss 3920  df-uni 4866  df-tr 5208  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-on 6329  df-lim 6330

This theorem is referenced by:  onzsl  7798  limuni3  7804  tfindsg2  7814  dfom2  7820  rdglim  8367  oalim  8469  omlim  8470  oelim  8471  oalimcl  8497  oaass  8498  omlimcl  8515  odi  8516  omass  8517  oen0  8524  oewordri  8530  oelim2  8533  oelimcl  8538  omabs  8589  r1lim  9696  alephordi  9996  cflm  10172  alephsing  10198  pwcfsdom  10506  winafp  10620  r1limwun  10659  omlimcl2  43596  oeord2lim  43663