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	$$⊢\left(A\in \mathrm{On}\wedge B\in A\right)\to \mathrm{Ord}B$$

Proof

Step	Hyp	Ref	Expression
1		onelon	$$⊢\left(A\in \mathrm{On}\wedge B\in A\right)\to B\in \mathrm{On}$$
2		eloni	$$⊢B\in \mathrm{On}\to \mathrm{Ord}B$$
3	1 2	syl	$$⊢\left(A\in \mathrm{On}\wedge B\in A\right)\to \mathrm{Ord}B$$