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

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

Proof of Theorem limuni
StepHypRef Expression
1 df-lim 4520 . 2  |-  ( Lim 
A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
21simp3bi 974 1  |-  ( Lim 
A  ->  A  =  U. A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    =/= wne 2543   (/)c0 3564   U.cuni 3950   Ord word 4514   Lim wlim 4516
This theorem is referenced by:  limuni2  4576  unizlim  4631  nlimsucg  4755  oa0r  6711  om1r  6715  oarec  6734  oeworde  6765  oeeulem  6773  infeq5i  7517  r1sdom  7626  rankxplim3  7731  cflm  8056  coflim  8067  cflim2  8069  cfss  8071  cfslbn  8073  limsucncmpi  25902
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-lim 4520
  Copyright terms: Public domain W3C validator