Theorem limuni 6368

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2928  ∅c0 4283  ∪ cuni 4859  Ord word 6305  Lim wlim 6307

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 6311

This theorem is referenced by:  limuni2  6369  unizlim  6430  nlimsucg  7772  oa0r  8453  om1r  8458  oarec  8477  oeworde  8508  oeeulem  8516  infeq5i  9526  r1sdom  9667  rankxplim3  9774  cflm  10141  coflim  10152  cflim2  10154  cfss  10156  cfslbn  10158  limsucncmpi  36485  limexissup  43320  limiun  43321  limexissupab  43322  dfom6  43570