Theorem limelon 6447

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 6443	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6391	. . 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 2107  Ord word 6382  Oncon0 6383  Lim wlim 6384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-v 3481  df-ss 3967  df-uni 4907  df-tr 5259  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-ord 6386  df-on 6387  df-lim 6388

This theorem is referenced by:  onzsl  7868  limuni3  7874  tfindsg2  7884  dfom2  7890  rdglim  8467  oalim  8571  omlim  8572  oelim  8573  oalimcl  8599  oaass  8600  omlimcl  8617  odi  8618  omass  8619  oen0  8625  oewordri  8631  oelim2  8634  oelimcl  8639  omabs  8690  r1lim  9813  alephordi  10115  cflm  10291  alephsing  10317  pwcfsdom  10624  winafp  10738  r1limwun  10777  omlimcl2  43259  oeord2lim  43327