Theorem limuni 6412

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

Syntax hints:   → wi 4   = wceq 1563   ≠ wne 2960  ∅c0 4288  ∪ cuni 4867  Ord word 6348  Lim wlim 6350

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 1103  df-lim 6354

This theorem is referenced by:  limuni2  6413  unizlim  6474  nlimsucg  7826  oa0r  8511  om1r  8516  oarec  8535  oeworde  8567  oeeulem  8575  infeq5i  9593  r1sdom  9734  rankxplim3  9841  cflm  10221  coflim  10233  cflim2  10235  cfss  10237  cfslbn  10239  limsucncmpi  36813  limexissup  43865  limiun  43866  limexissupab  43867  dfom6  44114