Theorem limelon 6247

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 6243	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
2		elong 6192	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ On ↔ Ord 𝐴))
3	1, 2	syl5ibr 248	. 2 ⊢ (𝐴 ∈ 𝐵 → (Lim 𝐴 → 𝐴 ∈ On))
4	3	imp 409	1 ⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2108  Ord word 6183  Oncon0 6184  Lim wlim 6185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-in 3941  df-ss 3950  df-uni 4831  df-tr 5164  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-ord 6187  df-on 6188  df-lim 6189

This theorem is referenced by:  onzsl  7553  limuni3  7559  tfindsg2  7568  dfom2  7574  rdglim  8054  oalim  8149  omlim  8150  oelim  8151  oalimcl  8178  oaass  8179  omlimcl  8196  odi  8197  omass  8198  oen0  8204  oewordri  8210  oelim2  8213  oelimcl  8218  omabs  8266  r1lim  9193  alephordi  9492  cflm  9664  alephsing  9690  pwcfsdom  9997  winafp  10111  r1limwun  10150