Theorem limuni 6446

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2959  ∅c0 4281  ∪ cuni 4870  Ord word 6382  Lim wlim 6384

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 6388

This theorem is used by:  limuni2  6447  unizlim  6508  nlimsucg  7880  oa0r  8577  om1r  8582  oarec  8601  oeworde  8633  oeeulem  8641  infeq5i  9667  r1sdom  9811  rankxplim3  9928  cflm  10357  coflim  10369  cfss  10373  cfslbn  10375  limsucncmpi  37424  limexissup  44486  limiun  44487  limexissupab  44488  dfom6  44735