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