Theorem sotri

Description: A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996) (Revised by Mario Carneiro, 10-May-2013)

	Ref	Expression
Hypotheses	soi.1	$$⊢R\mathrm{Or}S$$
	soi.2	$$⊢R\subseteq S\times S$$
Assertion	sotri	$$⊢\left(ARB\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	$$⊢ARB\to \left(A\in S\wedge B\in S\right)$$
4	3	simpld	$$⊢ARB\to A\in S$$
5	2	brel	$$⊢BRC\to \left(B\in S\wedge C\in S\right)$$
6	4 5	anim12i	$$⊢\left(ARB\wedge BRC\right)\to \left(A\in S\wedge \left(B\in S\wedge C\in S\right)\right)$$
7		sotr	$$⊢\left(R\mathrm{Or}S\wedge \left(A\in S\wedge B\in S\wedge C\in S\right)\right)\to \left(\left(ARB\wedge BRC\right)\to ARC\right)$$
8	1 7	mpan	$$⊢\left(A\in S\wedge B\in S\wedge C\in S\right)\to \left(\left(ARB\wedge BRC\right)\to ARC\right)$$
9	8	3expb	$$⊢\left(A\in S\wedge \left(B\in S\wedge C\in S\right)\right)\to \left(\left(ARB\wedge BRC\right)\to ARC\right)$$
10	6 9	mpcom	$$⊢\left(ARB\wedge BRC\right)\to ARC$$