Theorem limuni 6379

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933  ∅c0 4274  ∪ cuni 4851  Ord word 6316  Lim wlim 6318

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 6322

This theorem is referenced by:  limuni2  6380  unizlim  6441  nlimsucg  7786  oa0r  8466  om1r  8471  oarec  8490  oeworde  8522  oeeulem  8530  infeq5i  9548  r1sdom  9689  rankxplim3  9796  cflm  10163  coflim  10174  cflim2  10176  cfss  10178  cfslbn  10180  limsucncmpi  36643  limexissup  43727  limiun  43728  limexissupab  43729  dfom6  43976