Theorem limuni2

Description: The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006)

	Ref	Expression
Assertion	limuni2	⊢ ( Lim 𝐴 → Lim ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		limuni	⊢ ( Lim 𝐴 → 𝐴 = ∪ 𝐴 )
2		limeq	⊢ ( 𝐴 = ∪ 𝐴 → ( Lim 𝐴 ↔ Lim ∪ 𝐴 ) )
3	1 2	syl	⊢ ( Lim 𝐴 → ( Lim 𝐴 ↔ Lim ∪ 𝐴 ) )
4	3	ibi	⊢ ( Lim 𝐴 → Lim ∪ 𝐴 )