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

Theorem limuni 4947
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 4892 . 2  |-  ( Lim 
A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
21simp3bi 1013 1  |-  ( Lim 
A  ->  A  =  U. A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1395    =/= wne 2652   (/)c0 3793   U.cuni 4251   Ord word 4886   Lim wlim 4888
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 185  df-an 371  df-3an 975  df-lim 4892
This theorem is referenced by:  limuni2  4948  unizlim  5003  nlimsucg  6676  oa0r  7206  om1r  7210  oarec  7229  oeworde  7260  oeeulem  7268  infeq5i  8070  r1sdom  8209  rankxplim3  8316  cflm  8647  coflim  8658  cflim2  8660  cfss  8662  cfslbn  8664  limsucncmpi  30115
  Copyright terms: Public domain W3C validator