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

Theorem limuni 4452
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 4397 . 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 1623    =/= wne 2446   (/)c0 3455   U.cuni 3827   Ord word 4391   Lim wlim 4393
This theorem is referenced by:  limuni2  4453  unizlim  4509  nlimsucg  4633  oa0r  6537  om1r  6541  oarec  6560  oeworde  6591  oeeulem  6599  infeq5i  7337  r1sdom  7446  rankxplim3  7551  cflm  7876  coflim  7887  cflim2  7889  cfss  7891  cfslbn  7893  limsucncmpi  24884
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 4397
  Copyright terms: Public domain W3C validator