Theorem limelon 3727

Description: A limit ordinal class that is also a set is an ordinal number.

Assertion

Ref	Expression
limelon	|- ((A e. B /\ Lim A) -> A e. On)

Proof of Theorem limelon

Step	Hyp	Ref	Expression
1		elong 3665	. . 3 |- (A e. B -> (A e. On <-> Ord A))
2		limord 3723	. . 3 |- (Lim A -> Ord A)
3	1, 2	syl5bir 227	. 2 |- (A e. B -> (Lim A -> A e. On))
4	3	imp 377	1 |- ((A e. B /\ Lim A) -> A e. On)

Syntax hints:   -> wi 3   /\ wa 240   e. wcel 1300  Ord word 3656  Oncon0 3657  Lim wlim 3658

This theorem is referenced by:  onzsl 3928  limuni3 3936  tfindsg2 3945  dfom2 3951  rdglim 5156  oalim 5212  omlim 5213  oelim 5214  oalimcl 5242  oaass 5243  omlimcl 5257  odi 5258  omass 5259  oen0 5261  oewordri 5267  oelim2 5270  r1pwcl 5798  alephordi 6022  cflim 6057

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-rex 2110  df-v 2294  df-in 2603  df-ss 2605  df-uni 3178  df-tr 3412  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662

Copyright terms: Public domain