| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > limuni | Structured version Visualization version GIF version | ||
| Description: A limit ordinal is its own supremum (union). Lemma 2.13 of [Schloeder] p. 5. (Contributed by NM, 4-May-1995.) |
| Ref | Expression |
|---|---|
| limuni | ⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-lim 6389 | . 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | |
| 2 | 1 | simp3bi 1148 | 1 ⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ≠ wne 2940 ∅c0 4333 ∪ cuni 4907 Ord word 6383 Lim wlim 6385 |
| 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 6389 |
| This theorem is referenced by: limuni2 6446 unizlim 6507 nlimsucg 7863 oa0r 8576 om1r 8581 oarec 8600 oeworde 8631 oeeulem 8639 infeq5i 9676 r1sdom 9814 rankxplim3 9921 cflm 10290 coflim 10301 cflim2 10303 cfss 10305 cfslbn 10307 limsucncmpi 36446 limexissup 43294 limiun 43295 limexissupab 43296 dfom6 43544 |
| Copyright terms: Public domain | W3C validator |