Theorem limelon 5941

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 5937	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 5884	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
3	1, 2	syl5ibr 236	. 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On))
4	3	imp 444	1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2131  Ord word 5875  Oncon0 5876  Lim wlim 5877

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-v 3334  df-in 3714  df-ss 3721  df-uni 4581  df-tr 4897  df-po 5179  df-so 5180  df-fr 5217  df-we 5219  df-ord 5879  df-on 5880  df-lim 5881

This theorem is referenced by:  onzsl  7203  limuni3  7209  tfindsg2  7218  dfom2  7224  rdglim  7683  oalim  7773  omlim  7774  oelim  7775  oalimcl  7801  oaass  7802  omlimcl  7819  odi  7820  omass  7821  oen0  7827  oewordri  7833  oelim2  7836  oelimcl  7841  omabs  7888  r1lim  8800  alephordi  9079  cflm  9256  alephsing  9282  pwcfsdom  9589  winafp  9703  r1limwun  9742