Theorem limuni 6425

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

Syntax hints:   → wi 4   = wceq 1570   ≠ wne 2958  ∅c0 4287  ∪ cuni 4873  Ord word 6361  Lim wlim 6363

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 210  df-an 401  df-3an 1105  df-lim 6367

This theorem is referenced by:  limuni2  6426  unizlim  6487  nlimsucg  7839  oa0r  8524  om1r  8529  oarec  8548  oeworde  8580  oeeulem  8588  infeq5i  9606  r1sdom  9747  rankxplim3  9854  cflm  10234  coflim  10246  cflim2  10248  cfss  10250  cfslbn  10252  limsucncmpi  36937  limexissup  43991  limiun  43992  limexissupab  43993  dfom6  44240