Theorem limiun

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	$$⊢\mathrm{Lim}A\to A=\bigcup _{x\in A}x$$

Proof

Step	Hyp	Ref	Expression
1		limuni	$$⊢\mathrm{Lim}A\to A=\bigcup A$$
2		uniiun	$$⊢\bigcup A=\bigcup _{x\in A}x$$
3	1 2	eqtrdi	$$⊢\mathrm{Lim}A\to A=\bigcup _{x\in A}x$$