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

Theorem limuni 6445
Description: A limit ordinal is its own supremum (union). Lemma 2.13 of [Schloeder] p. 5. (Contributed by NM, 4-May-1995.)
Assertion
Ref Expression
limuni (Lim 𝐴𝐴 = 𝐴)

Proof of Theorem limuni
StepHypRef Expression
1 df-lim 6389 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp3bi 1148 1 (Lim 𝐴𝐴 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wne 2940  c0 4333   cuni 4907  Ord word 6383  Lim wlim 6385
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 207  df-an 396  df-3an 1089  df-lim 6389
This theorem is referenced by:  limuni2  6446  unizlim  6507  nlimsucg  7863  oa0r  8576  om1r  8581  oarec  8600  oeworde  8631  oeeulem  8639  infeq5i  9676  r1sdom  9814  rankxplim3  9921  cflm  10290  coflim  10301  cflim2  10303  cfss  10305  cfslbn  10307  limsucncmpi  36446  limexissup  43294  limiun  43295  limexissupab  43296  dfom6  43544
  Copyright terms: Public domain W3C validator