Theorem limuni 2284

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 2204	. 2 |- (Lim A <-> (Ord A /\ -. A = (/) /\ A = U.A))
2		3simp3 596	. 2 |- ((Ord A /\ -. A = (/) /\ A = U.A) -> A = U.A)
3	1, 2	sylbi 174	1 |- (Lim A -> A = U.A)

Syntax hints:  -. wn 1   -> wi 2   /\ w3a 581   = wceq 1091  (/)c0 1707  U.cuni 1919  Ord word 2198  Lim wlim 2200

This theorem is referenced by:  limsuclem 2360  nlimsuc 2363  unizlim 2364  dflim3 2368  oa0r 3141  om1r 3145  inf5 3472  cflim 3704

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583  df-lim 2204

metamath.org