Theorem limuni 6379

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2932  ∅c0 4285  ∪ cuni 4863  Ord word 6316  Lim wlim 6318

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 6322

This theorem is referenced by:  limuni2  6380  unizlim  6441  nlimsucg  7784  oa0r  8465  om1r  8470  oarec  8489  oeworde  8521  oeeulem  8529  infeq5i  9545  r1sdom  9686  rankxplim3  9793  cflm  10160  coflim  10171  cflim2  10173  cfss  10175  cfslbn  10177  limsucncmpi  36639  limexissup  43519  limiun  43520  limexissupab  43521  dfom6  43768