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\mathrm{Or}S$$
	soi.2	$$⊢R\subseteq S\times S$$
Assertion	sotri3	$$⊢\left(C\in S\wedge ARB\wedge \neg CRB\right)\to ARC$$

Proof

Step	Hyp	Ref	Expression
1		soi.1	$$⊢R\mathrm{Or}S$$
2		soi.2	$$⊢R\subseteq S\times S$$
3	2	brel	$$⊢ARB\to \left(A\in S\wedge B\in S\right)$$
4	3	simprd	$$⊢ARB\to B\in S$$
5		sotric	$$⊢\left(R\mathrm{Or}S\wedge \left(C\in S\wedge B\in S\right)\right)\to \left(CRB\leftrightarrow \neg \left(C=B\vee BRC\right)\right)$$
6	1 5	mpan	$$⊢\left(C\in S\wedge B\in S\right)\to \left(CRB\leftrightarrow \neg \left(C=B\vee BRC\right)\right)$$
7	6	con2bid	$$⊢\left(C\in S\wedge B\in S\right)\to \left(\left(C=B\vee BRC\right)\leftrightarrow \neg CRB\right)$$
8		breq2	$$⊢C=B\to \left(ARC\leftrightarrow ARB\right)$$
9	8	biimprd	$$⊢C=B\to \left(ARB\to ARC\right)$$
10	1 2	sotri	$$⊢\left(ARB\wedge BRC\right)\to ARC$$
11	10	expcom	$$⊢BRC\to \left(ARB\to ARC\right)$$
12	9 11	jaoi	$$⊢\left(C=B\vee BRC\right)\to \left(ARB\to ARC\right)$$
13	7 12	syl6bir	$$⊢\left(C\in S\wedge B\in S\right)\to \left(\neg CRB\to \left(ARB\to ARC\right)\right)$$
14	13	com3r	$$⊢ARB\to \left(\left(C\in S\wedge B\in S\right)\to \left(\neg CRB\to ARC\right)\right)$$
15	4 14	mpan2d	$$⊢ARB\to \left(C\in S\to \left(\neg CRB\to ARC\right)\right)$$
16	15	3imp21	$$⊢\left(C\in S\wedge ARB\wedge \neg CRB\right)\to ARC$$