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

Syntax hints:   → wi 4   = wceq 1534   ≠ wne 2935  ∅c0 4318  ∪ cuni 4903  Ord word 6362  Lim wlim 6364

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 206  df-an 396  df-3an 1087  df-lim 6368

This theorem is referenced by:  limuni2  6425  unizlim  6486  nlimsucg  7840  oa0r  8552  om1r  8557  oarec  8576  oeworde  8607  oeeulem  8615  infeq5i  9651  r1sdom  9789  rankxplim3  9896  cflm  10265  coflim  10276  cflim2  10278  cfss  10280  cfslbn  10282  limsucncmpi  35865  limexissup  42633  limiun  42634  limexissupab  42635  dfom6  42884