Theorem limuni 6385

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2932  ∅c0 4273  ∪ cuni 4850  Ord word 6322  Lim wlim 6324

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 6328

This theorem is referenced by:  limuni2  6386  unizlim  6447  nlimsucg  7793  oa0r  8473  om1r  8478  oarec  8497  oeworde  8529  oeeulem  8537  infeq5i  9557  r1sdom  9698  rankxplim3  9805  cflm  10172  coflim  10183  cflim2  10185  cfss  10187  cfslbn  10189  limsucncmpi  36627  limexissup  43709  limiun  43710  limexissupab  43711  dfom6  43958