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

Metamath Proof Explorer

Theorem limuni

Description: A limit ordinal is its own supremum (union). Lemma 2.13 of Schloeder p. 5. (Contributed by NM, 4-May-1995)

		Ref	Expression
	Assertion	limuni	$⊢ Lim A \to A = ⋃ A$

Step	Hyp	Ref	Expression
1		df-lim	$⊢ Lim A \leftrightarrow (Ord A \land A \neq \emptyset \land A = ⋃ A)$
2	1	simp3bi	$⊢ Lim A \to A = ⋃ A$