Metamath Proof Explorer

Theorem onelord

Description: Every element of a ordinal is an ordinal. Lemma 1.3 of Schloeder p. 1. Based on onelon and eloni . (Contributed by RP, 15-Jan-2025)

		Ref	Expression
	Assertion	onelord	$⊢ (A \in On \land B \in A) \to Ord B$

Step	Hyp	Ref	Expression
1		onelon	$⊢ (A \in On \land B \in A) \to B \in On$
2		eloni	$⊢ B \in On \to Ord B$
3	1 2	syl	$⊢ (A \in On \land B \in A) \to Ord B$