Theorem limord 3018

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 2943	. 2 |- (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))
2		3simp1 786	. 2 |- ((Ord A /\ A =/= (/) /\ A = U.A) -> Ord A)
3	1, 2	sylbi 199	1 |- (Lim A -> Ord A)

Syntax hints:   -> wi 3   /\ w3a 773   = wceq 953   =/= wne 1577  (/)c0 2270  U.cuni 2493  Ord word 2937  Lim wlim 2939

This theorem is referenced by:  0ellim 3021  limelon 3022  ordzsl 3106  dflim3 3108  limsuc 3110  limsssuc 3111  limomss 3127  ordom 3131  limom 3136  rdglim2 3934  oarec 4180  odi 4194  oelim2 4206  oaabs 4236  limenpsi 4485  limensuci 4486  r1ord 4627  r1val1 4630

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 775  df-lim 2943

Copyright terms: Public domain