Theorem limuni 6414

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2932  ∅c0 4308  ∪ cuni 4883  Ord word 6351  Lim wlim 6353

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 6357

This theorem is referenced by:  limuni2  6415  unizlim  6477  nlimsucg  7837  oa0r  8550  om1r  8555  oarec  8574  oeworde  8605  oeeulem  8613  infeq5i  9650  r1sdom  9788  rankxplim3  9895  cflm  10264  coflim  10275  cflim2  10277  cfss  10279  cfslbn  10281  limsucncmpi  36463  limexissup  43305  limiun  43306  limexissupab  43307  dfom6  43555