Theorem limuni 6404

Description: A limit ordinal is its own supremum (union). Lemma 2.13 of [Schloeder] p. 5. (Contributed by NM, 4-May-1995.)

Assertion

Ref	Expression
limuni	⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴)

Proof of Theorem limuni

Step	Hyp	Ref	Expression
1		df-lim 6347	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
2	1	simp3bi 1159	1 ⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴)

Syntax hints:   → wi 4   = wceq 1559   ≠ wne 2956  ∅c0 4285  ∪ cuni 4864  Ord word 6341  Lim wlim 6343

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 209  df-an 400  df-3an 1099  df-lim 6347

This theorem is referenced by:  limuni2  6405  unizlim  6466  nlimsucg  7818  oa0r  8502  om1r  8507  oarec  8526  oeworde  8558  oeeulem  8566  infeq5i  9588  r1sdom  9729  rankxplim3  9836  cflm  10203  coflim  10215  cflim2  10217  cfss  10219  cfslbn  10221  limsucncmpi  36769  limexissup  43822  limiun  43823  limexissupab  43824  dfom6  44071