Theorem limuni 6426

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2941  ∅c0 4323  ∪ cuni 4909  Ord word 6364  Lim wlim 6366

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 206  df-an 398  df-3an 1090  df-lim 6370

This theorem is referenced by:  limuni2  6427  unizlim  6488  nlimsucg  7831  oa0r  8538  om1r  8543  oarec  8562  oeworde  8593  oeeulem  8601  infeq5i  9631  r1sdom  9769  rankxplim3  9876  cflm  10245  coflim  10256  cflim2  10258  cfss  10260  cfslbn  10262  limsucncmpi  35378  limexissup  42079  limiun  42080  limexissupab  42081  dfom6  42330