Metamath Proof Explorer


Theorem ordtr2

Description: Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)

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

Proof

Step Hyp Ref Expression
1 ordelord
 |-  ( ( Ord C /\ B e. C ) -> Ord B )
2 1 ex
 |-  ( Ord C -> ( B e. C -> Ord B ) )
3 2 ancld
 |-  ( Ord C -> ( B e. C -> ( B e. C /\ Ord B ) ) )
4 3 anc2li
 |-  ( Ord C -> ( B e. C -> ( Ord C /\ ( B e. C /\ Ord B ) ) ) )
5 ordelpss
 |-  ( ( Ord B /\ Ord C ) -> ( B e. C <-> B C. C ) )
6 sspsstr
 |-  ( ( A C_ B /\ B C. C ) -> A C. C )
7 6 expcom
 |-  ( B C. C -> ( A C_ B -> A C. C ) )
8 5 7 syl6bi
 |-  ( ( Ord B /\ Ord C ) -> ( B e. C -> ( A C_ B -> A C. C ) ) )
9 8 expcom
 |-  ( Ord C -> ( Ord B -> ( B e. C -> ( A C_ B -> A C. C ) ) ) )
10 9 com23
 |-  ( Ord C -> ( B e. C -> ( Ord B -> ( A C_ B -> A C. C ) ) ) )
11 10 imp32
 |-  ( ( Ord C /\ ( B e. C /\ Ord B ) ) -> ( A C_ B -> A C. C ) )
12 11 com12
 |-  ( A C_ B -> ( ( Ord C /\ ( B e. C /\ Ord B ) ) -> A C. C ) )
13 4 12 syl9
 |-  ( Ord C -> ( A C_ B -> ( B e. C -> A C. C ) ) )
14 13 impd
 |-  ( Ord C -> ( ( A C_ B /\ B e. C ) -> A C. C ) )
15 14 adantl
 |-  ( ( Ord A /\ Ord C ) -> ( ( A C_ B /\ B e. C ) -> A C. C ) )
16 ordelpss
 |-  ( ( Ord A /\ Ord C ) -> ( A e. C <-> A C. C ) )
17 15 16 sylibrd
 |-  ( ( Ord A /\ Ord C ) -> ( ( A C_ B /\ B e. C ) -> A e. C ) )