Theorem limord 3028

Description: A limit ordinal is ordinal.

Assertion

Ref	Expression
limord	|- (Lim A -> Ord A)

Proof of Theorem limord

Step	Hyp	Ref	Expression
1		df-lim 2953	. 2 |- (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))
2		3simp1 788	. 2 |- ((Ord A /\ A =/= (/) /\ A = U.A) -> Ord A)
3	1, 2	sylbi 199	1 |- (Lim A -> Ord A)

Syntax hints:   -> wi 3   /\ w3a 775   = wceq 956   =/= wne 1585  (/)c0 2280  U.cuni 2503  Ord word 2947  Lim wlim 2949

This theorem is referenced by:  0ellim 3031  limelon 3032  ordzsl 3116  dflim3 3118  limsuc 3120  limsssuc 3121  limomss 3137  ordom 3141  limom 3146  rdglim2 3949  oarec 4196  odi 4210  oelim2 4222  oaabs 4252  limenpsi 4505  limensuci 4506  r1ord 4655  r1val1 4658

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777  df-lim 2953

Copyright terms: Public domain