Theorem limord 2283

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 2204	. 2 ⊢ (Lim A ↔ (Ord A ∧ ¬ A = ∅ ∧ A = ∪A))
2		3simp1 594	. 2 ⊢ ((Ord A ∧ ¬ A = ∅ ∧ A = ∪A) → Ord A)
3	1, 2	sylbi 174	1 ⊢ (Lim A → Ord A)

Syntax hints:  ¬ wn 1   → wi 2   ∧ w3a 581   = wceq 1091  ∅c0 1707  ∪cuni 1919  Ord word 2198  Lim wlim 2200

This theorem is referenced by:  0ellim 2285  limelon 2286  limsuc 2361  limsssuc 2362  ordzsl 2366  dflim3 2368  limomss 2378  ordom 2382  limom 2387  rdglim2 2987  limenpsi 3400  limensuci 3401  r1ord 3499  r1val1 3502

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583  df-lim 2204

metamath.org