Theorem limuni2

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

	Ref	Expression
Assertion	limuni2	$$⊢\mathrm{Lim}A\to \mathrm{Lim}\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		limuni	$$⊢\mathrm{Lim}A\to A=\bigcup A$$
2		limeq	$$⊢A=\bigcup A\to \left(\mathrm{Lim}A\leftrightarrow \mathrm{Lim}\bigcup A\right)$$
3	1 2	syl	$$⊢\mathrm{Lim}A\to \left(\mathrm{Lim}A\leftrightarrow \mathrm{Lim}\bigcup A\right)$$
4	3	ibi	$$⊢\mathrm{Lim}A\to \mathrm{Lim}\bigcup A$$