Theorem limuni 6397

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2926  ∅c0 4299  ∪ cuni 4874  Ord word 6334  Lim wlim 6336

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 6340

This theorem is referenced by:  limuni2  6398  unizlim  6460  nlimsucg  7821  oa0r  8505  om1r  8510  oarec  8529  oeworde  8560  oeeulem  8568  infeq5i  9596  r1sdom  9734  rankxplim3  9841  cflm  10210  coflim  10221  cflim2  10223  cfss  10225  cfslbn  10227  limsucncmpi  36440  limexissup  43277  limiun  43278  limexissupab  43279  dfom6  43527