Metamath Proof Explorer

Theorem oneptr

Description: The strict order on the ordinals is transitive. Theorem 1.9(ii) of Schloeder p. 1. (Contributed by RP, 15-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 epweon 
 |-  _E We On
2 weso 
 |-  ( _E We On -> _E Or On )
3 sopo 
 |-  ( _E Or On -> _E Po On )
4 potr 
 |-  ( ( _E Po On /\ ( A e. On /\ B e. On /\ C e. On ) ) -> ( ( A _E B /\ B _E C ) -> A _E C ) )
5 4 ex 
 |-  ( _E Po On -> ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A _E B /\ B _E C ) -> A _E C ) ) )
6 3 5 syl 
 |-  ( _E Or On -> ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A _E B /\ B _E C ) -> A _E C ) ) )
7 1 2 6 mp2b 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A _E B /\ B _E C ) -> A _E C ) )