Theorem sotri2

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	sotri2	|- ( ( A e. S /\ -. B R A /\ B R C ) -> 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	|- ( B R C -> ( B e. S /\ C e. S ) )
4	3	simpld	|- ( B R C -> B e. S )
5		sotric	|- ( ( R Or S /\ ( B e. S /\ A e. S ) ) -> ( B R A <-> -. ( B = A \/ A R B ) ) )
6	1 5	mpan	|- ( ( B e. S /\ A e. S ) -> ( B R A <-> -. ( B = A \/ A R B ) ) )
7	6	con2bid	|- ( ( B e. S /\ A e. S ) -> ( ( B = A \/ A R B ) <-> -. B R A ) )
8		breq1	|- ( B = A -> ( B R C <-> A R C ) )
9	8	biimpd	|- ( B = A -> ( B R C -> A R C ) )
10	1 2	sotri	|- ( ( A R B /\ B R C ) -> A R C )
11	10	ex	|- ( A R B -> ( B R C -> A R C ) )
12	9 11	jaoi	|- ( ( B = A \/ A R B ) -> ( B R C -> A R C ) )
13	7 12	syl6bir	|- ( ( B e. S /\ A e. S ) -> ( -. B R A -> ( B R C -> A R C ) ) )
14	13	com3r	|- ( B R C -> ( ( B e. S /\ A e. S ) -> ( -. B R A -> A R C ) ) )
15	4 14	mpand	|- ( B R C -> ( A e. S -> ( -. B R A -> A R C ) ) )
16	15	3imp231	|- ( ( A e. S /\ -. B R A /\ B R C ) -> A R C )