Metamath Proof Explorer

Theorem ontr2

Description: Transitive law for ordinal numbers. Exercise 3 of TakeutiZaring p. 40. (Contributed by NM, 6-Nov-2003)

Ref Expression
Assertion ontr2 
|- ( ( A e. On /\ C e. On ) -> ( ( A C_ B /\ B e. C ) -> A e. C ) )

Proof

Step Hyp Ref Expression
1 eloni 
 |-  ( A e. On -> Ord A )
2 eloni 
 |-  ( C e. On -> Ord C )
3 ordtr2 
 |-  ( ( Ord A /\ Ord C ) -> ( ( A C_ B /\ B e. C ) -> A e. C ) )
4 1 2 3 syl2an 
 |-  ( ( A e. On /\ C e. On ) -> ( ( A C_ B /\ B e. C ) -> A e. C ) )