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\mathrm{Or}S$$
	soi.2	$$⊢R\subseteq S\times S$$
Assertion	sotri2	$$⊢\left(A\in S\wedge \neg BRA\wedge BRC\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	$$⊢BRC\to \left(B\in S\wedge C\in S\right)$$
4	3	simpld	$$⊢BRC\to B\in S$$
5		sotric	$$⊢\left(R\mathrm{Or}S\wedge \left(B\in S\wedge A\in S\right)\right)\to \left(BRA\leftrightarrow \neg \left(B=A\vee ARB\right)\right)$$
6	1 5	mpan	$$⊢\left(B\in S\wedge A\in S\right)\to \left(BRA\leftrightarrow \neg \left(B=A\vee ARB\right)\right)$$
7	6	con2bid	$$⊢\left(B\in S\wedge A\in S\right)\to \left(\left(B=A\vee ARB\right)\leftrightarrow \neg BRA\right)$$
8		breq1	$$⊢B=A\to \left(BRC\leftrightarrow ARC\right)$$
9	8	biimpd	$$⊢B=A\to \left(BRC\to ARC\right)$$
10	1 2	sotri	$$⊢\left(ARB\wedge BRC\right)\to ARC$$
11	10	ex	$$⊢ARB\to \left(BRC\to ARC\right)$$
12	9 11	jaoi	$$⊢\left(B=A\vee ARB\right)\to \left(BRC\to ARC\right)$$
13	7 12	syl6bir	$$⊢\left(B\in S\wedge A\in S\right)\to \left(\neg BRA\to \left(BRC\to ARC\right)\right)$$
14	13	com3r	$$⊢BRC\to \left(\left(B\in S\wedge A\in S\right)\to \left(\neg BRA\to ARC\right)\right)$$
15	4 14	mpand	$$⊢BRC\to \left(A\in S\to \left(\neg BRA\to ARC\right)\right)$$
16	15	3imp231	$$⊢\left(A\in S\wedge \neg BRA\wedge BRC\right)\to ARC$$