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	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐴 ) → Ord 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		onelon	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ On )
2		eloni	⊢ ( 𝐵 ∈ On → Ord 𝐵 )
3	1 2	syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝐴 ) → Ord 𝐵 )