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

Theorem limuni 6249
 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 6194 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp3bi 1141 1 (Lim 𝐴𝐴 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1530   ≠ wne 3021  ∅c0 4295  ∪ cuni 4837  Ord word 6188  Lim wlim 6190 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 208  df-an 397  df-3an 1083  df-lim 6194 This theorem is referenced by:  limuni2  6250  unizlim  6305  nlimsucg  7545  oa0r  8154  om1r  8159  oarec  8178  oeworde  8209  oeeulem  8217  infeq5i  9088  r1sdom  9192  rankxplim3  9299  cflm  9661  coflim  9672  cflim2  9674  cfss  9676  cfslbn  9678  limsucncmpi  33677  dfom6  39763
 Copyright terms: Public domain W3C validator