Theorem sotri3

Description: A transitivity relation. (Read A < B and B <_ C implies A < C .) (Contributed by Mario Carneiro, 10-May-2013)

	Ref	Expression
Hypotheses	soi.1	|- R Or S
	soi.2	|- R C_ ( S X. S )
Assertion	sotri3	|- ( ( C e. S /\ A R B /\ -. C R B ) -> A R C )

Proof

Step	Hyp	Ref	Expression
1		soi.1	|- R Or S
2		soi.2	|- R C_ ( S X. S )
3	2	brel	|- ( A R B -> ( A e. S /\ B e. S ) )
4	3	simprd	|- ( A R B -> B e. S )
5		sotric	|- ( ( R Or S /\ ( C e. S /\ B e. S ) ) -> ( C R B <-> -. ( C = B \/ B R C ) ) )
6	1 5	mpan	|- ( ( C e. S /\ B e. S ) -> ( C R B <-> -. ( C = B \/ B R C ) ) )
7	6	con2bid	|- ( ( C e. S /\ B e. S ) -> ( ( C = B \/ B R C ) <-> -. C R B ) )
8		breq2	|- ( C = B -> ( A R C <-> A R B ) )
9	8	biimprd	|- ( C = B -> ( A R B -> A R C ) )
10	1 2	sotri	|- ( ( A R B /\ B R C ) -> A R C )
11	10	expcom	|- ( B R C -> ( A R B -> A R C ) )
12	9 11	jaoi	|- ( ( C = B \/ B R C ) -> ( A R B -> A R C ) )
13	7 12	biimtrrdi	|- ( ( C e. S /\ B e. S ) -> ( -. C R B -> ( A R B -> A R C ) ) )
14	13	com3r	|- ( A R B -> ( ( C e. S /\ B e. S ) -> ( -. C R B -> A R C ) ) )
15	4 14	mpan2d	|- ( A R B -> ( C e. S -> ( -. C R B -> A R C ) ) )
16	15	3imp21	|- ( ( C e. S /\ A R B /\ -. C R B ) -> A R C )