Theorem limuni 6418

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2956  ∅c0 4279  ∪ cuni 4867  Ord word 6354  Lim wlim 6356

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-lim 6360

This theorem is used by:  limuni2  6419  unizlim  6480  nlimsucg  7842  oa0r  8530  om1r  8535  oarec  8554  oeworde  8586  oeeulem  8594  infeq5i  9621  r1sdom  9764  rankxplim3  9879  cflm  10308  coflim  10320  cflim2  10322  cfss  10324  cfslbn  10326  limsucncmpi  37203  limexissup  44241  limiun  44242  limexissupab  44243  dfom6  44490