Theorem limelon 6427

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 6423	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6369	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
3	1, 2	imbitrrid 249	. 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On))
4	3	imp 412	1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Ord word 6360  Oncon0 6361  Lim wlim 6362

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-v 3453  df-ss 3916  df-uni 4868  df-tr 5213  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6364  df-on 6365  df-lim 6366

This theorem is used by:  onzsl  7855  limuni3  7861  tfindsg2  7871  dfom2  7877  rdglim  8427  oalim  8533  omlim  8534  oelim  8535  oalimcl  8561  oaass  8562  omlimcl  8579  odi  8580  omass  8581  oen0  8588  oewordri  8594  oelim2  8597  oelimcl  8602  omabs  8653  r1lim  9772  alephordi  10146  cflm  10320  alephsing  10347  pwcfsdom  10661  winafp  10775  r1limwun  10814  omlimcl2  44228  oeord2lim  44295