Theorem limelon 5788

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1990  Ord word 5722  Oncon0 5723  Lim wlim 5724

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-uni 4437  df-tr 4753  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-ord 5726  df-on 5727  df-lim 5728

This theorem is referenced by:  onzsl  7046  limuni3  7052  tfindsg2  7061  dfom2  7067  rdglim  7522  oalim  7612  omlim  7613  oelim  7614  oalimcl  7640  oaass  7641  omlimcl  7658  odi  7659  omass  7660  oen0  7666  oewordri  7672  oelim2  7675  oelimcl  7680  omabs  7727  r1lim  8635  alephordi  8897  cflm  9072  alephsing  9098  pwcfsdom  9405  winafp  9519  r1limwun  9558