Metamath Proof Explorer

Theorem ordtr3

Description: Transitive law for ordinal classes. (Contributed by Mario Carneiro, 30-Dec-2014) (Proof shortened by JJ, 24-Sep-2021)

Ref Expression
Assertion ordtr3 
|- ( ( Ord B /\ Ord C ) -> ( A e. B -> ( A e. C \/ C e. B ) ) )

Proof

Step Hyp Ref Expression
1 nelss 
 |-  ( ( A e. B /\ -. A e. C ) -> -. B C_ C )
2 1 adantl 
 |-  ( ( ( Ord B /\ Ord C ) /\ ( A e. B /\ -. A e. C ) ) -> -. B C_ C )
3 ordtri1 
 |-  ( ( Ord B /\ Ord C ) -> ( B C_ C <-> -. C e. B ) )
4 3 con2bid 
 |-  ( ( Ord B /\ Ord C ) -> ( C e. B <-> -. B C_ C ) )
5 4 adantr 
 |-  ( ( ( Ord B /\ Ord C ) /\ ( A e. B /\ -. A e. C ) ) -> ( C e. B <-> -. B C_ C ) )
6 2 5 mpbird 
 |-  ( ( ( Ord B /\ Ord C ) /\ ( A e. B /\ -. A e. C ) ) -> C e. B )
7 6 expr 
 |-  ( ( ( Ord B /\ Ord C ) /\ A e. B ) -> ( -. A e. C -> C e. B ) )
8 7 orrd 
 |-  ( ( ( Ord B /\ Ord C ) /\ A e. B ) -> ( A e. C \/ C e. B ) )
9 8 ex 
 |-  ( ( Ord B /\ Ord C ) -> ( A e. B -> ( A e. C \/ C e. B ) ) )