Theorem limuni 6430

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2961  ∅c0 4289  ∪ cuni 4877  Ord word 6366  Lim wlim 6368

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 6372

This theorem is used by:  limuni2  6431  unizlim  6492  nlimsucg  7847  oa0r  8532  om1r  8537  oarec  8556  oeworde  8588  oeeulem  8596  infeq5i  9615  r1sdom  9756  rankxplim3  9863  cflm  10251  coflim  10263  cflim2  10265  cfss  10267  cfslbn  10269  limsucncmpi  36997  limexissup  44049  limiun  44050  limexissupab  44051  dfom6  44298