This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limuni2

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

		Ref	Expression
	Assertion	limuni2	$⊢ Lim A \to Lim ⋃ A$

Step	Hyp	Ref	Expression
1		limuni	$⊢ Lim A \to A = ⋃ A$
2		limeq	$⊢ A = ⋃ A \to (Lim A \leftrightarrow Lim ⋃ A)$
3	1 2	syl	$⊢ Lim A \to (Lim A \leftrightarrow Lim ⋃ A)$
4	3	ibi	$⊢ Lim A \to Lim ⋃ A$