Theorem limuni 6425

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ≠ wne 2955  ∅c0 4278  ∪ cuni 4866  Ord word 6361  Lim wlim 6363

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 6367

This theorem is used by:  limuni2  6426  unizlim  6487  nlimsucg  7854  oa0r  8550  om1r  8555  oarec  8574  oeworde  8606  oeeulem  8614  infeq5i  9641  r1sdom  9785  rankxplim3  9902  cflm  10331  coflim  10343  cfss  10347  cfslbn  10349  limsucncmpi  37326  limexissup  44377  limiun  44378  limexissupab  44379  dfom6  44626