Theorem limuni 6445

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2940  ∅c0 4333  ∪ cuni 4907  Ord word 6383  Lim wlim 6385

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 6389

This theorem is referenced by:  limuni2  6446  unizlim  6507  nlimsucg  7863  oa0r  8576  om1r  8581  oarec  8600  oeworde  8631  oeeulem  8639  infeq5i  9676  r1sdom  9814  rankxplim3  9921  cflm  10290  coflim  10301  cflim2  10303  cfss  10305  cfslbn  10307  limsucncmpi  36446  limexissup  43294  limiun  43295  limexissupab  43296  dfom6  43544