Theorem limuni 6373

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925  ∅c0 4286  ∪ cuni 4861  Ord word 6310  Lim wlim 6312

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 6316

This theorem is referenced by:  limuni2  6374  unizlim  6435  nlimsucg  7782  oa0r  8463  om1r  8468  oarec  8487  oeworde  8518  oeeulem  8526  infeq5i  9551  r1sdom  9689  rankxplim3  9796  cflm  10163  coflim  10174  cflim2  10176  cfss  10178  cfslbn  10180  limsucncmpi  36418  limexissup  43254  limiun  43255  limexissupab  43256  dfom6  43504