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

Theorem limuni 5968
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 5913 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp3bi 1177 1 (Lim 𝐴𝐴 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wne 2937  c0 4079   cuni 4594  Ord word 5907  Lim wlim 5909
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 198  df-an 385  df-3an 1109  df-lim 5913
This theorem is referenced by:  limuni2  5969  unizlim  6024  nlimsucg  7240  oa0r  7823  om1r  7828  oarec  7847  oeworde  7878  oeeulem  7886  infeq5i  8748  r1sdom  8852  rankxplim3  8959  cflm  9325  coflim  9336  cflim2  9338  cfss  9340  cfslbn  9342  limsucncmpi  32815
  Copyright terms: Public domain W3C validator