This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi 
 |-  ( ( 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 ) )