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

Metamath Proof Explorer

Theorem limelon

Description: A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004)

		Ref	Expression
	Assertion	limelon	$⊢ (A \in B \land Lim A) \to A \in On$

Step	Hyp	Ref	Expression
1		limord	$⊢ Lim A \to Ord A$
2		elong	$⊢ A \in B \to (A \in On \leftrightarrow Ord A)$
3	1 2	imbitrrid	$⊢ A \in B \to (Lim A \to A \in On)$
4	3	imp	$⊢ (A \in B \land Lim A) \to A \in On$