Theorem limuni 3029

Description: A limit ordinal is its own supremum (union).

Assertion

Ref	Expression
limuni	|- (Lim A -> A = U.A)

Proof of Theorem limuni

Step	Hyp	Ref	Expression
1		df-lim 2953	. 2 |- (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))
2		3simp3 790	. 2 |- ((Ord A /\ A =/= (/) /\ A = U.A) -> A = U.A)
3	1, 2	sylbi 199	1 |- (Lim A -> A = U.A)

Syntax hints:   -> wi 3   /\ w3a 775   = wceq 956   =/= wne 1585  (/)c0 2280  U.cuni 2503  Ord word 2947  Lim wlim 2949

This theorem is referenced by:  limuni2 3030  nlimsucg 3112  unizlim 3113  dflim3 3118  oa0r 4173  om1r 4177  oeworde 4220  oaabs 4252  infeq5 4621  rankxplim3 4714  cflim 4909

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777  df-lim 2953

Copyright terms: Public domain