Theorem limelon 5931

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

Syntax hints:   → wi 4   ∧ wa 382   ∈ wcel 2144  Ord word 5865  Oncon0 5866  Lim wlim 5867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-v 3351  df-in 3728  df-ss 3735  df-uni 4573  df-tr 4885  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-ord 5869  df-on 5870  df-lim 5871

This theorem is referenced by:  onzsl  7192  limuni3  7198  tfindsg2  7207  dfom2  7213  rdglim  7674  oalim  7765  omlim  7766  oelim  7767  oalimcl  7793  oaass  7794  omlimcl  7811  odi  7812  omass  7813  oen0  7819  oewordri  7825  oelim2  7828  oelimcl  7833  omabs  7880  r1lim  8798  alephordi  9096  cflm  9273  alephsing  9299  pwcfsdom  9606  winafp  9720  r1limwun  9759