Theorem limuni 6394

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 6337	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
2	1	simp3bi 1147	1 ⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925  ∅c0 4296  ∪ cuni 4871  Ord word 6331  Lim wlim 6333

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 207  df-an 396  df-3an 1088  df-lim 6337

This theorem is referenced by:  limuni2  6395  unizlim  6457  nlimsucg  7818  oa0r  8502  om1r  8507  oarec  8526  oeworde  8557  oeeulem  8565  infeq5i  9589  r1sdom  9727  rankxplim3  9834  cflm  10203  coflim  10214  cflim2  10216  cfss  10218  cfslbn  10220  limsucncmpi  36433  limexissup  43270  limiun  43271  limexissupab  43272  dfom6  43520