Theorem trrelind

Description: The intersection of transitive relations is a transitive relation. (Contributed by RP, 24-Dec-2019)

	Ref	Expression
Hypotheses	trrelind.r	$$⊢\phi \to R\circ R\subseteq R$$
	trrelind.s	$$⊢\phi \to S\circ S\subseteq S$$
	trrelind.t	$$⊢\phi \to T=R\cap S$$
Assertion	trrelind	$$⊢\phi \to T\circ T\subseteq T$$

Proof

Step	Hyp	Ref	Expression
1		trrelind.r	$$⊢\phi \to R\circ R\subseteq R$$
2		trrelind.s	$$⊢\phi \to S\circ S\subseteq S$$
3		trrelind.t	$$⊢\phi \to T=R\cap S$$
4		inss1	$$⊢R\cap S\subseteq R$$
5	4	a1i	$$⊢\phi \to R\cap S\subseteq R$$
6	1 5 5	trrelssd	$$⊢\phi \to \left(R\cap S\right)\circ \left(R\cap S\right)\subseteq R$$
7		inss2	$$⊢R\cap S\subseteq S$$
8	7	a1i	$$⊢\phi \to R\cap S\subseteq S$$
9	2 8 8	trrelssd	$$⊢\phi \to \left(R\cap S\right)\circ \left(R\cap S\right)\subseteq S$$
10	6 9	ssind	$$⊢\phi \to \left(R\cap S\right)\circ \left(R\cap S\right)\subseteq R\cap S$$
11	3 3	coeq12d	$$⊢\phi \to T\circ T=\left(R\cap S\right)\circ \left(R\cap S\right)$$
12	10 11 3	3sstr4d	$$⊢\phi \to T\circ T\subseteq T$$