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 1153	1 ⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴)

Syntax hints:   → wi 4   = wceq 1547   ≠ wne 2935  ∅c0 4268  ∪ cuni 4845  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 208  df-an 397  df-3an 1094  df-lim 6322

This theorem is referenced by:  limuni2  6380  unizlim  6441  nlimsucg  7789  oa0r  8470  om1r  8475  oarec  8494  oeworde  8526  oeeulem  8534  infeq5i  9555  r1sdom  9696  rankxplim3  9803  cflm  10170  coflim  10181  cflim2  10183  cfss  10185  cfslbn  10187  limsucncmpi  36680  limexissup  43733  limiun  43734  limexissupab  43735  dfom6  43982