Theorem limuni 6373

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2929  ∅c0 4282  ∪ cuni 4858  Ord word 6310  Lim wlim 6312

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 6316

This theorem is referenced by:  limuni2  6374  unizlim  6435  nlimsucg  7778  oa0r  8459  om1r  8464  oarec  8483  oeworde  8514  oeeulem  8522  infeq5i  9533  r1sdom  9674  rankxplim3  9781  cflm  10148  coflim  10159  cflim2  10161  cfss  10163  cfslbn  10165  limsucncmpi  36510  limexissup  43399  limiun  43400  limexissupab  43401  dfom6  43649