Theorem limuni 6456

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 2946  ∅c0 4352  ∪ cuni 4931  Ord word 6394  Lim wlim 6396

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 1089  df-lim 6400

This theorem is referenced by:  limuni2  6457  unizlim  6518  nlimsucg  7879  oa0r  8594  om1r  8599  oarec  8618  oeworde  8649  oeeulem  8657  infeq5i  9705  r1sdom  9843  rankxplim3  9950  cflm  10319  coflim  10330  cflim2  10332  cfss  10334  cfslbn  10336  limsucncmpi  36411  limexissup  43243  limiun  43244  limexissupab  43245  dfom6  43493