Theorem limuni 6387

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933  ∅c0 4287  ∪ cuni 4865  Ord word 6324  Lim wlim 6326

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 1089  df-lim 6330

This theorem is referenced by:  limuni2  6388  unizlim  6449  nlimsucg  7794  oa0r  8475  om1r  8480  oarec  8499  oeworde  8531  oeeulem  8539  infeq5i  9557  r1sdom  9698  rankxplim3  9805  cflm  10172  coflim  10183  cflim2  10185  cfss  10187  cfslbn  10189  limsucncmpi  36658  limexissup  43632  limiun  43633  limexissupab  43634  dfom6  43881