Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  limuni Structured version   Visualization version   GIF version

Theorem limuni 5773
 Description: A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.)
Assertion
Ref Expression
limuni (Lim 𝐴𝐴 = 𝐴)

Proof of Theorem limuni
StepHypRef Expression
1 df-lim 5716 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp3bi 1076 1 (Lim 𝐴𝐴 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1481   ≠ wne 2791  ∅c0 3907  ∪ cuni 4427  Ord word 5710  Lim wlim 5712 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038  df-lim 5716 This theorem is referenced by:  limuni2  5774  unizlim  5832  nlimsucg  7027  oa0r  7603  om1r  7608  oarec  7627  oeworde  7658  oeeulem  7666  infeq5i  8518  r1sdom  8622  rankxplim3  8729  cflm  9057  coflim  9068  cflim2  9070  cfss  9072  cfslbn  9074  limsucncmpi  32419
 Copyright terms: Public domain W3C validator