Theorem limelon 6382

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 6378	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6325	. . 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 6316  Oncon0 6317  Lim wlim 6318

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 3432  df-ss 3907  df-uni 4852  df-tr 5194  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-lim 6322

This theorem is referenced by:  onzsl  7790  limuni3  7796  tfindsg2  7806  dfom2  7812  rdglim  8358  oalim  8460  omlim  8461  oelim  8462  oalimcl  8488  oaass  8489  omlimcl  8506  odi  8507  omass  8508  oen0  8515  oewordri  8521  oelim2  8524  oelimcl  8529  omabs  8580  r1lim  9687  alephordi  9987  cflm  10163  alephsing  10189  pwcfsdom  10497  winafp  10611  r1limwun  10650  omlimcl2  43688  oeord2lim  43755