Description: A limit ordinal is the union of its elements, indexed union version. Lemma 2.13 of Schloeder p. 5. See limuni . (Contributed by RP, 27-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | limiun | |- ( Lim A -> A = U_ x e. A x ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | limuni | |- ( Lim A -> A = U. A ) |
|
| 2 | uniiun | |- U. A = U_ x e. A x |
|
| 3 | 1 2 | eqtrdi | |- ( Lim A -> A = U_ x e. A x ) |