Theorem limuni 6424

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2957  ∅c0 4282  ∪ cuni 4870  Ord word 6360  Lim wlim 6362

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 6366

This theorem is used by:  limuni2  6425  unizlim  6486  nlimsucg  7842  oa0r  8529  om1r  8534  oarec  8553  oeworde  8585  oeeulem  8593  infeq5i  9619  r1sdom  9760  rankxplim3  9867  cflm  10255  coflim  10267  cflim2  10269  cfss  10271  cfslbn  10273  limsucncmpi  37072  limexissup  44130  limiun  44131  limexissupab  44132  dfom6  44379