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	⊢ ( Lim 𝐴 → 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		limuni	⊢ ( Lim 𝐴 → 𝐴 = ∪ 𝐴 )
2		uniiun	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
3	1 2	eqtrdi	⊢ ( Lim 𝐴 → 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥 )