Theorem limuni 6446

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

Syntax hints:   → wi 4   = wceq 1536   ≠ wne 2937  ∅c0 4338  ∪ cuni 4911  Ord word 6384  Lim wlim 6386

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 6390

This theorem is referenced by:  limuni2  6447  unizlim  6508  nlimsucg  7862  oa0r  8574  om1r  8579  oarec  8598  oeworde  8629  oeeulem  8637  infeq5i  9673  r1sdom  9811  rankxplim3  9918  cflm  10287  coflim  10298  cflim2  10300  cfss  10302  cfslbn  10304  limsucncmpi  36427  limexissup  43270  limiun  43271  limexissupab  43272  dfom6  43520