Theorem limuni 6424

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

Syntax hints:   → wi 4   = wceq 1567   ≠ wne 2964  ∅c0 4294  ∪ cuni 4876  Ord word 6360  Lim wlim 6362

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 6366

This theorem is referenced by:  limuni2  6425  unizlim  6486  nlimsucg  7838  oa0r  8523  om1r  8528  oarec  8547  oeworde  8579  oeeulem  8587  infeq5i  9605  r1sdom  9746  rankxplim3  9853  cflm  10233  coflim  10245  cflim2  10247  cfss  10249  cfslbn  10251  limsucncmpi  36879  limexissup  43934  limiun  43935  limexissupab  43936  dfom6  44183