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 e. On /\ B e. A ) -> Ord B )

Proof

Step Hyp Ref Expression
1 onelon 
 |-  ( ( A e. On /\ B e. A ) -> B e. On )
2 eloni 
 |-  ( B e. On -> Ord B )
3 1 2 syl 
 |-  ( ( A e. On /\ B e. A ) -> Ord B )