Theorem limelon 6092

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 6088	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6037	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
3	1, 2	syl5ibr 238	. 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On))
4	3	imp 398	1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2050  Ord word 6028  Oncon0 6029  Lim wlim 6030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-in 3836  df-ss 3843  df-uni 4713  df-tr 5031  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-ord 6032  df-on 6033  df-lim 6034

This theorem is referenced by:  onzsl  7377  limuni3  7383  tfindsg2  7392  dfom2  7398  rdglim  7866  oalim  7959  omlim  7960  oelim  7961  oalimcl  7987  oaass  7988  omlimcl  8005  odi  8006  omass  8007  oen0  8013  oewordri  8019  oelim2  8022  oelimcl  8027  omabs  8074  r1lim  8995  alephordi  9294  cflm  9470  alephsing  9496  pwcfsdom  9803  winafp  9917  r1limwun  9956