Theorem limelon 6430

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 6426	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6372	. . 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 2146  Ord word 6363  Oncon0 6364  Lim wlim 6365

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-v 3459  df-ss 3923  df-uni 4875  df-tr 5221  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368  df-lim 6369

This theorem is used by:  onzsl  7844  limuni3  7850  tfindsg2  7860  dfom2  7866  rdglim  8415  oalim  8519  omlim  8520  oelim  8521  oalimcl  8547  oaass  8548  omlimcl  8565  odi  8566  omass  8567  oen0  8574  oewordri  8580  oelim2  8583  oelimcl  8588  omabs  8639  r1lim  9747  alephordi  10070  cflm  10244  alephsing  10271  pwcfsdom  10579  winafp  10693  r1limwun  10732  omlimcl2  44002  oeord2lim  44069