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

Theorem limuni 4468
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 4413 . 2  |-  ( Lim 
A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
21simp3bi 972 1  |-  ( Lim 
A  ->  A  =  U. A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    =/= wne 2459   (/)c0 3468   U.cuni 3843   Ord word 4407   Lim wlim 4409
This theorem is referenced by:  limuni2  4469  unizlim  4525  nlimsucg  4649  oa0r  6553  om1r  6557  oarec  6576  oeworde  6607  oeeulem  6615  infeq5i  7353  r1sdom  7462  rankxplim3  7567  cflm  7892  coflim  7903  cflim2  7905  cfss  7907  cfslbn  7909  limsucncmpi  24956
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 177  df-an 360  df-3an 936  df-lim 4413
  Copyright terms: Public domain W3C validator