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

Theorem limuni 5445
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 5390 . 2  |-  ( Lim 
A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
21simp3bi 1022 1  |-  ( Lim 
A  ->  A  =  U. A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    =/= wne 2599   (/)c0 3704   U.cuni 4162   Ord word 5384   Lim wlim 5386
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 188  df-an 372  df-3an 984  df-lim 5390
This theorem is referenced by:  limuni2  5446  unizlim  5501  nlimsucg  6627  oa0r  7195  om1r  7199  oarec  7218  oeworde  7249  oeeulem  7257  infeq5i  8094  r1sdom  8197  rankxplim3  8304  cflm  8631  coflim  8642  cflim2  8644  cfss  8646  cfslbn  8648  limsucncmpi  31054
  Copyright terms: Public domain W3C validator